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

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

1 2 next

  1. Claessen, Koen; Lillieström, Ann: Handling transitive relations in first-order automated reasoning (2021)
  2. Cristiá, Maximiliano; Rossi, Gianfranco: Solving quantifier-free first-order constraints over finite sets and binary relations (2020)
  3. Hallahan, William T.; Zhai, Ennan; Piskac, Ruzica: Automated repair by example for firewalls (2020)
  4. Milicevic, Aleksandar; Near, Joseph P.; Kang, Eunsuk; Jackson, Daniel: Alloy*: a general-purpose higher-order relational constraint solver (2019)
  5. Paulson, Lawrence C.; Nipkow, Tobias; Wenzel, Makarius: From LCF to Isabelle/HOL (2019)
  6. Porncharoenwase, Sorawee; Nelson, Tim; Krishnamurthi, Shriram: CompoSAT: specification-guided coverage for model finding (2018)
  7. 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)
  8. Devriendt, Jo; Bogaerts, Bart; Bruynooghe, Maurice; Denecker, Marc: On local domain symmetry for model expansion (2016)
  9. Reynolds, Andrew; Blanchette, Jasmin Christian; Cruanes, Simon; Tinelli, Cesare: Model finding for recursive functions in SMT (2016)
  10. Iser, Markus; Manthey, Norbert; Sinz, Carsten: Recognition of nested gates in CNF formulas (2015)
  11. Saghafi, Salman; Danas, Ryan; Dougherty, Daniel J.: Exploring theories with a model-finding assistant (2015)
  12. Plagge, Daniel; Leuschel, Michael: Validating B,Z and TLA(^ + ) using ProB and Kodkod (2012) ioport
  13. Blanchette, Jasmin Christian; Bulwahn, Lukas; Nipkow, Tobias: Automatic proof and disproof in Isabelle/HOL (2011)
  14. Blanchette, Jasmin Christian; Krauss, Alexander: Monotonicity inference for higher-order formulas (2011)
  15. Cuervo Parrino, Bruno; Galeotti, Juan Pablo; Garbervetsky, Diego; Frias, Marcelo F.: A dataflow analysis to improve SAT-based bounded program verification (2011) ioport
  16. Gopinath, Divya; Malik, Muhammad Zubair; Khurshid, Sarfraz: Specification-based program repair using SAT (2011)
  17. Leuschel, Michael; Falampin, Jérôme; Fritz, Fabian; Plagge, Daniel: Automated property verification for large scale B models with ProB (2011) ioport
  18. Blanchette, Jasmin Christian; Claessen, Koen: Generating counterexamples for structural inductions by exploiting nonstandard models (2010)
  19. Blanchette, Jasmin Christian; Nipkow, Tobias: Nitpick: a counterexample generator for higher-order logic based on a relational model finder (2010)
  20. Dunets, Andriy; Schellhorn, Gerhard; Reif, Wolfgang: Automated flaw detection in algebraic specifications (2010)

1 2 next

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