Kodkod: A Relational Model Finder

By Emina Torlak, Daniel Jackson. International Conference on Tools and Algorithms for Construction and Analysis of Systems, 2007

554 citations recorded by the source corpus.

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

Mathematizing C++ concurrency (2011, methodology): “We have also explored the use of a model generator (the SAT-solver-based Kodkod [TJ07], via the Isabelle Nitpick interface [BN10]) to .nd executions more ef.ciently, albeit with less assurance.”
Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder (2010, methodology): “It works by translating higher-order formulas to first-order relational logic (FORL) and invoking the highly-optimized SATbased Kodkod model finder [21] to solve these.”
Optimizing database-backed applications with query synthesis (2013, background): “Symmetries have been shown to be one of sources of inefficiency in constraint solvers [11, 34].”
Answer Set Solving in Practice (2012, methodology): “Interesting combinations of modeling and solving in SAT are provided by kodkod (Torlak and Jackson, 2007), a constraint solver for first-order logic with relations, and npspec (Cadoli and Schaerf, 2005), a Datalog-like language based on minimal models semantics.”