swMATH ID: 7090
Software Authors: Torlak, Emina; Jackson, Daniel
Description: Kodkod: A relational model finder. The key design challenges in the construction of a SAT-based relational model finder are described, and novel techniques are proposed to address them. An efficient model finder must have a mechanism for specifying partial solutions, an effective symmetry detection and breaking scheme, and an economical translation from relational to boolean logic. These desiderata are addressed with three new techniques: a symmetry detection algorithm that works in the presence of partial solutions, a sparse-matrix representation of relations, and a compact representation of boolean formulas inspired by boolean expression diagrams and reduced boolean circuits. The presented techniques have been implemented and evaluated, with promising results.
Homepage: http://alloy.mit.edu/kodkod/
Related Software: z3; Isabelle/HOL; Nitpick; Mace4; Isabelle; Coq; TPTP; Prover9; HOL; PVS; ML; Isar; VAMPIRE; margrave; TestEra; MiniSat; ProB; SmallCheck; QuickCheck; Sledgehammer
Referenced in: 20 Publications
Further Publications: http://alloy.mit.edu/kodkod/pubs.html

Standard Articles

1 Publication describing the Software, including 1 Publication in zbMATH Year
Kodkod: A relational model finder. Zbl 1186.68304
Torlak, Emina; Jackson, Daniel

Referencing Publications by Year