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 23 articles , 1 standard article )

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

1 2 next

  1. Cristiá, Maximiliano; Rossi, Gianfranco: Solving quantifier-free first-order constraints over finite sets and binary relations (2020)
  2. Milicevic, Aleksandar; Near, Joseph P.; Kang, Eunsuk; Jackson, Daniel: Alloy*: a general-purpose higher-order relational constraint solver (2019)
  3. Paulson, Lawrence C.; Nipkow, Tobias; Wenzel, Makarius: From LCF to Isabelle/HOL (2019)
  4. Biendarra, Julian; Blanchette, Jasmin Christian; Bouzy, Aymeric; Desharnais, Martin; Fleury, Mathias; Hölzl, Johannes; Kunčar, Ondřej; Lochbihler, Andreas; Meier, Fabian; Panny, Lorenz; Popescu, Andrei; Sternagel, Christian; Thiemann, René; Traytel, Dmitriy: Foundational (co)datatypes and (co)recursion for higher-order logic (2017)
  5. Devriendt, Jo; Bogaerts, Bart; Bruynooghe, Maurice; Denecker, Marc: On local domain symmetry for model expansion (2016)
  6. Reynolds, Andrew; Blanchette, Jasmin Christian; Cruanes, Simon; Tinelli, Cesare: Model finding for recursive functions in SMT (2016)
  7. Iser, Markus; Manthey, Norbert; Sinz, Carsten: Recognition of nested gates in CNF formulas (2015)
  8. Saghafi, Salman; Danas, Ryan; Dougherty, Daniel J.: Exploring theories with a model-finding assistant (2015)
  9. Plagge, Daniel; Leuschel, Michael: Validating B,Z and TLA(^ + ) using ProB and Kodkod (2012) ioport
  10. Blanchette, Jasmin Christian; Bulwahn, Lukas; Nipkow, Tobias: Automatic proof and disproof in Isabelle/HOL (2011)
  11. Blanchette, Jasmin Christian; Krauss, Alexander: Monotonicity inference for higher-order formulas (2011)
  12. Cuervo Parrino, Bruno; Galeotti, Juan Pablo; Garbervetsky, Diego; Frias, Marcelo F.: A dataflow analysis to improve SAT-based bounded program verification (2011) ioport
  13. Gopinath, Divya; Malik, Muhammad Zubair; Khurshid, Sarfraz: Specification-based program repair using SAT (2011)
  14. Leuschel, Michael; Falampin, Jérôme; Fritz, Fabian; Plagge, Daniel: Automated property verification for large scale B models with ProB (2011) ioport
  15. Blanchette, Jasmin Christian; Claessen, Koen: Generating counterexamples for structural inductions by exploiting nonstandard models (2010)
  16. Blanchette, Jasmin Christian; Nipkow, Tobias: Nitpick: a counterexample generator for higher-order logic based on a relational model finder (2010)
  17. Dunets, Andriy; Schellhorn, Gerhard; Reif, Wolfgang: Automated flaw detection in algebraic specifications (2010)
  18. Jackson, Ethan; Sztipanovits, Janos: Formalizing the structural semantics of domain-specific modeling languages (2009) ioport
  19. Dunets, Andriy; Schellhorn, Gerhard; Reif, Wolfgang: Bounded relational analysis of free data types (2008)
  20. Dunets, Andriy; Schellhorn, Gerhard; Reif, Wolfgang: Automating algebraic specifications of non-freely generated data types (2008)

1 2 next

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