1. Armin Biere, Alessandro Cimatti, Edmund Clarke & Yunshan Zhu (1999): Symbolic Model Checking without BDDs. In: W. Rance Cleaveland: Tools and Algorithms for the Construction and Analysis of Systems. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 193–207, doi:10.1007/3-540-49059-0_14.
  2. Nikolaj Bjørner, Arie Gurfinkel, Kenneth L. McMillan & Andrey Rybalchenko (2015): Horn Clause Solvers for Program Verification. In: Fields of Logic and Computation II - Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday, pp. 24–51, doi:10.1007/978-3-319-23534-9_2.
  3. Martin Blicha, Antti E. J. Hyvärinen, Jan Kofroň & Natasha Sharygina (2019): Decomposing Farkas Interpolants. In: Tomáš Vojnar & Lijun Zhang: Tools and Algorithms for the Construction and Analysis of Systems. Springer International Publishing, Cham, pp. 3–20, doi:10.1007/978-3-030-17462-0_1.
  4. Martin Blicha, Antti E. J. Hyvärinen, Matteo Marescotti & Natasha Sharygina (2020): A Cooperative Parallelization Approach for Property-Directed k-Induction. In: Dirk Beyer & Damien Zufferey: Verification, Model Checking, and Abstract Interpretation. Springer International Publishing, Cham, pp. 270–292, doi:10.1007/978-3-030-39322-9_13.
  5. Aaron R. Bradley (2011): SAT-Based Model Checking without Unrolling. In: VMCAI, LNCS 6538. Springer, pp. 70–87, doi:10.1007/978-3-642-18275-4_7.
  6. Alessandro Cimatti, Alberto Griggio, Sergio Mover & Stefano Tonetta (2016): Infinite-state invariant checking with IC3 and predicate abstraction. Formal Methods Syst. Des. 49(3), pp. 190–218, doi:10.1007/s10703-016-0257-4.
  7. Alessandro Cimatti, Alberto Griggio, Bastiaan Schaafsma & Roberto Sebastiani (2013): The MathSAT5 SMT Solver. In: Nir Piterman & Scott Smolka: Proceedings of TACAS, LNCS 7795. Springer, doi:10.1007/978-3-642-36742-7_7.
  8. Daniel Dietsch, Matthias Heizmann, Jochen Hoenicke, Alexander Nutz & Andreas Podelski (2019): Ultimate TreeAutomizer (CHC-COMP Tool Description). In: HCVS/PERR@ETAPS, EPTCS 296, pp. 42–47, doi:10.4204/EPTCS.296.7.
  9. Bruno Dutertre (2014): Yices 2.2. In: Armin Biere & Roderick Bloem: Computer-Aided Verification (CAV'2014), LNCS 8559. Springer, pp. 737–744, doi:10.1007/978-3-319-08867-9_49.
  10. Sergey Grebenshchikov, Nuno P. Lopes, Corneliu Popeea & Andrey Rybalchenko (2012): Synthesizing Software Verifiers from Proof Rules. In: PLDI. ACM, pp. 405–416, doi:10.1145/2254064.2254112.
  11. Alberto Griggio (Accessed 2020): Open-source IC3 Modulo Theories with Implicit Predicate Abstraction. Available at
  12. Matthias Heizmann, Yu-Fang Chen, Daniel Dietsch, Marius Greitschus, Jochen Hoenicke, Yong Li, Alexander Nutz, Betim Musa, Christian Schilling, Tanja Schindler & Andreas Podelski (2018): Ultimate Automizer and the Search for Perfect Interpolants - (Competition Contribution). In: TACAS (2), LNCS 10806. Springer, pp. 447–451, doi:10.1007/978-3-319-89963-3_30.
  13. Matthias Heizmann, Jochen Hoenicke & Andreas Podelski (2013): Software Model Checking for People Who Love Automata. In: CAV, LNCS 8044. Springer, pp. 36–52, doi:10.1007/978-3-642-39799-8_2.
  14. Jochen Hoenicke & Tanja Schindler (2018): Efficient Interpolation for the Theory of Arrays. In: IJCAR, LNCS 10900. Springer, pp. 549–565, doi:10.1007/978-3-319-94205-6_36.
  15. Hossein Hojjat & Philipp Rümmer (2018): The ELDARICA Horn Solver. In: Nikolaj Bjørner & Arie Gurfinkel: 2018 Formal Methods in Computer Aided Design, FMCAD. IEEE, pp. 1–7, doi:10.23919/FMCAD.2018.8603013.
  16. Antti E. J. Hyvärinen, Matteo Marescotti, Leonardo Alt & Natasha Sharygina (2016): OpenSMT2: An SMT Solver for Multi-core and Cloud Computing. In: Nadia Creignou & Daniel Le Berre: Theory and Applications of Satisfiability Testing – SAT 2016. Springer International Publishing, Cham, pp. 547–553, doi:10.1007/978-3-319-40970-2_35.
  17. Dejan Jovanovi\'c & Bruno Dutertre (2016): Property-directed k-induction. In: 2016 Formal Methods in Computer-Aided Design (FMCAD), pp. 85–92, doi:10.1109/FMCAD.2016.7886665.
  18. Hari Govind V K, YuTing Chen, Sharon Shoham & Arie Gurfinkel (2020): Global Guidance for Local Generalization in Model Checking. In: Computer Aided Verification - 32nd International Conference, CAV 2020. To appear.
  19. Anvesh Komuravelli, Arie Gurfinkel & Sagar Chaki (2016): SMT-based model checking for recursive programs. Formal Methods Syst. Des. 48(3), pp. 175–205, doi:10.1007/s10703-016-0249-4.
  20. Daniel Kroening, Alex Groce & Edmund M. Clarke (2004): Counterexample Guided Abstraction Refinement Via Program Execution. In: ICFEM, LNCS 3308. Springer, pp. 224–238, doi:10.1007/978-3-540-30482-1_23.
  21. Matteo Marescotti, Antti Hyv\ "arinen & Natasha Sharygina (2018): SMTS: Distributed, Visualized Constraint Solving. In: Gilles Barthe, Geoff Sutcliffe & Margus Veanes: LPAR-22. 22nd International Conference on Logic for Programming, Artificial Intelligence and Reasoning, EPiC Series in Computing 57. EasyChair, pp. 534–542, doi:10.29007/fhgn.
  22. Philipp Rümmer (2008): A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic. In: Proceedings, 15th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LNCS 5330. Springer, pp. 274–289, doi:10.1007/978-3-540-89439-1_20.
  23. Yuki Satake, Hiroshi Unno & Hinata Yanagi (2020): Probabilistic Inference for Predicate Constraint Satisfaction. In: Proceedings of AAAI 2020. To appear.
  24. Aaron Stump, Geoff Sutcliffe & Cesare Tinelli (2014): StarExec: A Cross-Community Infrastructure for Logic Solving. In: Stéphane Demri, Deepak Kapur & Christoph Weidenbach: Automated Reasoning - 7th International Joint Conference, IJCAR, LNCS 8562. Springer, pp. 367–373, doi:10.1007/978-3-319-08587-6_28.
  25. Xiaozhen Zhang & Weiqiang Kong (2020): Facilitating CHC Solving with Improving Interpolation Abstraction Exploration. To appear.

Comments and questions to:
For website issues: