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.

References in zbMATH (referenced in 19 articles , 1 standard article )

Showing results 1 to 19 of 19.
Sorted by year (citations)

  1. Devriendt, Jo; Bogaerts, Bart; Bruynooghe, Maurice; Denecker, Marc: On local domain symmetry for model expansion (2016)
  2. Reynolds, Andrew; Blanchette, Jasmin Christian; Cruanes, Simon; Tinelli, Cesare: Model finding for recursive functions in SMT (2016)
  3. Iser, Markus; Manthey, Norbert; Sinz, Carsten: Recognition of nested gates in CNF formulas (2015)
  4. Saghafi, Salman; Danas, Ryan; Dougherty, Daniel J.: Exploring theories with a model-finding assistant (2015)
  5. Plagge, Daniel; Leuschel, Michael: Validating B,Z and TLA$^ + $ using ProB and Kodkod (2012) ioport
  6. Blanchette, Jasmin Christian; Bulwahn, Lukas; Nipkow, Tobias: Automatic proof and disproof in Isabelle/HOL (2011)
  7. Blanchette, Jasmin Christian; Krauss, Alexander: Monotonicity inference for higher-order formulas (2011)
  8. Cuervo Parrino, Bruno; Galeotti, Juan Pablo; Garbervetsky, Diego; Frias, Marcelo F.: A dataflow analysis to improve SAT-based bounded program verification (2011) ioport
  9. Gopinath, Divya; Malik, Muhammad Zubair; Khurshid, Sarfraz: Specification-based program repair using SAT (2011)
  10. Leuschel, Michael; Falampin, Jér^ome; Fritz, Fabian; Plagge, Daniel: Automated property verification for large scale B models with ProB (2011) ioport
  11. Blanchette, Jasmin Christian; Claessen, Koen: Generating counterexamples for structural inductions by exploiting nonstandard models (2010)
  12. Blanchette, Jasmin Christian; Nipkow, Tobias: Nitpick: a counterexample generator for higher-order logic based on a relational model finder (2010)
  13. Dunets, Andriy; Schellhorn, Gerhard; Reif, Wolfgang: Automated flaw detection in algebraic specifications (2010)
  14. Jackson, Ethan; Sztipanovits, Janos: Formalizing the structural semantics of domain-specific modeling languages (2009) ioport
  15. Dunets, Andriy; Schellhorn, Gerhard; Reif, Wolfgang: Bounded relational analysis of free data types (2008)
  16. Dunets, Andriy; Schellhorn, Gerhard; Reif, Wolfgang: Automating algebraic specifications of non-freely generated data types (2008)
  17. Narain, Sanjai; Levin, Gary; Malik, Sharad; Kaul, Vikram: Declarative infrastructure configuration synthesis and debugging (2008) ioport
  18. Ramananandro, Tahina: Mondex, an electronic purse: specification and refinement checks with the alloy model-finding method (2008) ioport
  19. Torlak, Emina; Jackson, Daniel: Kodkod: A relational model finder (2007)

Further publications can be found at: http://alloy.mit.edu/kodkod/pubs.html