• Created by Unknown User (leberre_1@touchstonenetwork.net), last modified on Jun 16, 2011 07:53

You are viewing an old version of this page. View the current version.

Compare with Current View Page History

« Previous Version 14 Next »

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

html: Security restricted macro is not allowed. An edit restriction is required that matches the macro authorization list. —

an illustrative encoding of a behavior that the model should allow or prohibit. Given these inputs, the tool outputs a trace of the program for which the assertions are satisfied or, if no such trace exists, it outputs a minimal subset of the program and memory model constraints that are unsatisfiable.

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.

  File Modified
No files shared here yet.
  • No labels