Kodkod is an efficient SAT-based analysis engine for first order logic with relations, transitive closure, and partial instances. The current prototype, which includes a finite model finder and a minimal unsatisfiable core extractor, is being used as a backend to the Karun, Forge, and Miniatur code checkers, a course scheduler, the Alloy Analyzer 4.0, a network configuration tool, etc.
Unlike traditional model finders (e.g. Alloy Analyzer 3, Paradox, and MACE), Kodkod is designed to take advantage of partial instance information, by allowing the user to specify a partial solution that the model finder then completes. In a network configuration problem, for example, the set of all active nodes is known. Any solution to a formula encoding the configuration problem must include all active nodes. The binding from the relation representing active nodes to the set of all active nodes is therefore a partial instance of the configuration formula.
publications
- E. Torlak, F. Chang and D. Jackson. Finding Minimal Unsatisfiable Cores of Declarative Specifications. Formal Methods (FM'08). Turku, Finland, May 2008. (PDF)
- E. Torlak and D. Jackson. Kodkod: A Relational Model Finder. Tools and Algorithms for Construction and Analysis of Systems (TACAS '07). Braga, Portugal, March 2007. (PDF) (slides)
- E. Torlak and G. Dennis. Kodkod for Alloy Users. First ACM Alloy Workshop. Portland, Oregon, November 2006. (PDF) (slides)
- E. Torlak and D. Jackson. The Design of a Relational Engine. MIT CSAIL Technical Report MIT-CSAIL-TR-2006-068, September 2006. (PDF)
related publications
- M. Taghdiri. Automating Modular Program Verification by Refining Specifications. PhD thesis, Massachusetts Institute of Technology, December 2007.
- J. Dolby, M. Vaziri and F. Tip. Finding Bugs Efficiently with a SAT Solver. In ESEC-FSE '07, Dubrovnik, Croatia, September 2007.
- E. Uzuncaova, D. Garcia, S. Khurshid and D. Batory. A Specification-Based Approach to Testing Software Product Lines. In ESEC-FSE '07, Dubrovnik, Croatia, September 2007.
- G. Dennis, F. Chang and D. Jackson. Modular Verification of Code. In ISSTA'06, Portland, Maine, July 2006.
- V. Yeung. Declarative Configuration Applied to Course Scheduling. Master's thesis, Massachusetts Institute of Technology, June 2006.
download
- kodkod.jar - kodkod binaries and sources, released under the MIT license; requires java 1.5x and a SAT library.
- SAT4J, windows.zip, mac-ppc.zip, mac-intel.zip, linux.zip - SAT libraries. The SAT4J library is platform independent, others are specific to the Windows XP, Mac OS X (power pc), Mac OS X (intel), and Linux platforms respectively.
- docs.zip - API documentation.
- examples.jar - binaries and documented java source files demonstrating the use of the kodkod API. Sample usage (k = directory containing platform specific binaries, kodkod.jar, and examples.jar):
- $ cd k
- $ unzip mac-intel.zip
- $ chmod u+x x86-mac/*.*
- $ java -cp examples.jar:kodkod.jar -Djava.library.path=x86-mac examples.Sudoku
contact