Alloy/Kodkod and Applications
Kodkod is an efficient SAT-based constraint solver for first order logic with relations, transitive closure, and partial models. It provides analyses for both satisfiable and unsatisfiable problems: finite model finder for the former and a minimal unsatisfiable core extractor for the latter. Kodkod has been used in many applications, including code checking, test-case generation, declarative configuration, and lightweight analysis of formal specifications written in Alloy, UML, and Isabelle/HOL.
This talk will focus on MemSAT, a recent application of Kodkod to debugging and reasoning about memory models. MemSAT takes as input an axiomatic specification of a memory model and a multi-threaded test program containing assertions. The test program and the assertions comprise a litmus test for the memory model
MemSAT has been applied to several existing memory models and their published litmus tests, including the current Java Memory Model by Manson et al., and a revised version of it by Sevcik and Aspinall. The results revealed subtle discrepancies between what was expected and the actual results of test programs.
Emina Torlak, LogicBlox, Inc., Atlanta, GA, USA
Emina Torlak received her Ph.D. (2009), M.Eng. (2004) and B.Sc. (2003) in Computer Science from MIT. Her primary research interests are in the development and application of scalable tools for lightweight formal methods, program analysis, debugging and testing. She designed and implemented Kodkod, a relational constraint solver with numerous applications to design analysis, code checking, test-case generation, and declarative configuration. Emina is currently a Senior Computer Scientist at LogicBlox, where she is working on specification-based testing of online analytical processing applications. Prior to joining LogicBlox, she was a Research Staff Member at the IBM T. J. Watson Research Center, where her work focused on the analysis of weak memory models, symbolic debugging, and resource leak detection.