1. Wolfgang Ahrendt, Bernhard Beckert, Richard Bubel, Reinher Hähnle, Peter H. Schmitt & Mattias Ulbrich (2016): Deductive Software Verification — The KeY Book — From Theory to Practice. LNCS 10001. Springer International Publishing, Cham, doi:10.1007/978-3-319-49812-6.
  2. Mike Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs & K. Rustan M. Leino (2005): Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In: FMCO 2005: Formal Methods for Components and Objects, LNCS 4111. Springer, Berlin, Germany, pp. 364–387, doi:10.1007/11804192_17.
  3. Clark Barrett, Pascal Fontaine & Cesare Tinelli (2016): The Satisfiability Modulo Theories Library (SMT-LIB). Available at
  4. Jasmin Christian Blanchette, Sascha Böhme & Lawrence C. Paulson (2011): Extending Sledgehammer with SMT Solvers. In: CADE-23: Automated Deduction, 23rd International Conference, LNCS 6803. Springer, Berlin, Germany, pp. 116–130, doi:10.1007/978-3-642-22438-6_11.
  5. Jasmin Christian Blanchette & Tobias Nipkow (2010): Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder. In: ITP 2010: Interactive Theorem Proving, LNCS 6172. Springer, Berlin, Germany, pp. 131–146, doi:10.1007/978-3-642-14052-5_11.
  6. David Déharbe, Pascal Fontaine, Yoann Guyot & Laurent Voisin (2012): SMT Solvers for Rodin. In: ABZ 2012: Abstract State Machines, Alloy, B, VDM, and Z, Third International Conference, Pisa, Italy, June 18–21, 2012, LNCS 7316. Springer, Berlin, Germany, pp. 194–207, doi:10.1007/978-3-642-30885-7_14.
  7. Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller & Guy Katz (2017): SMTCoq: A Plug-In for Integrating SMT Solvers into Coq. In: CAV 2017: Computer Aided Verification, Heidelberg, Germany, July 24–28, 2017, LNCS 10427. Springer, Cham, Switzerland, pp. 126–133, doi:10.1007/978-3-319-63390-9_7.
  8. Aboubakr Achraf El Ghazi & Mana Taghdiri (2015): Analyzing Alloy Formulas using an SMT Solver: A Case Study. AFM10: Automated Formal Methods, July 14, 2010, Edinburgh, UK. Available at
  9. Daniel Jackson (2000): Automating First-Order Relational Logic. In: SIGSOFT'00/FSE-8 International Symposium, San Diego, California, USA, November 2000, SIGSOFT Software Engineering Notes 25(6). ACM, New York, NY, USA, pp. 130–139, doi:10.1145/355045.355063.
  10. K. Rustan M. Leino (2010): Dafny: An Automatic Program Verifier for Functional Correctness. In: Edmund M. Clarke & Andrei Voronkov: LPAR-16: Logic Programming and Automated Reasoning, 16th International Conference, Dakar, Senegal, April 25–May 1, 2010, LNCS 6355. Springer, Berlin, Germany, pp. 348–370, doi:10.1007/978-3-642-17511-4_20.
  11. Hsin-Hung Lin & Bow-Yaw Wang (2017): Releasing VDM Proof Obligations with SMT Solvers. In: MEMOCODE '17: 15th ACM-IEEE International Conference on Formal Methods and Models for System Design, Vienna, Austria, September 29–October 2, 2017. ACM, New York, NY, USA, pp. 132135, doi:10.1145/3127041.3127066.
  12. Stephan Merz & Hernán Vanzetto (2016): Encoding TLA^+ into Many-Sorted First-Order Logic. In: ABZ 2016: Abstract State Machines, Alloy, B, TLA, VDM, and Z: 5th International Conference, Linz, Austria, May 23–27, 2016, LNCS 9675. Springer, Cham, Switzerland, pp. 54–69, doi:10.1007/978-3-319-33600-8_3.
  13. Giles Reger, Martin Suda & Andrei Voronkov (2017): Instantiation and Pretending to be an SMT Solver with Vampire. In: SMT 2017 Workshop, Heidelberg, Germany, July 22–23, 2017, CEUR Workshop Proceedings 1889, pp. 63–75. Available at
  14. Franz-Xaver Reichl (2020): The Integration of SMT Solvers into the RISCAL Model Checker. Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz, Austria. Available at
  15. Wolfgang Schreiner (2018): Validating Mathematical Theories and Algorithms with RISCAL. In: CICM 2018, 11th Conference on Intelligent Computer Mathematics, Hagenberg, Austria, August 13–17, LNCS/Lecture Notes in Artificial Intelligence 11006. Springer, Berlin, pp. 248–254, doi:10.1007/978-3-319-96812-4_21.
  16. Wolfgang Schreiner (2019): The RISC Algorithm Language (RISCAL). Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. Available at
  17. Wolfgang Schreiner & Franz-Xaver Reichl (2020): Mathematical Model Checking Based on Semantics and SMT. Transactions on Internet Research 16(2), pp. 4–13. Available at
  18. Wolfgang Schreiner & Franz-Xaver Reichl (2021): Semantic Evaluation versus SMT Solving in the RISCAL Model Checker. Technical Report 21-11. RISC, Johannes Kepler University, Linz, Austria. Available at
  19. Wolfgang Schreiner, William Steingartner & Valerie Novitzká (2020): A Novel Categorical Approach to the Semantics of Relational First-Order Logic. Symmetry 12(10), doi:10.3390/sym12101584.
  20. SMT-COMP (2021): SMT-COMP: The International Satisfiability Modulo Theories (SMT) Competition.. Available at
  21. Emina Torlak & Daniel Jackson (2007): Kodkod: A Relational Model Finder. In: TACAS 2007: Tools and Algorithms for the Construction and Analysis of Systems, 3th International Conference, Braga, Portugal, March 24–April 1, 2007, LNCS 4424. Springer, Berlin, Germany, pp. 632–647, doi:10.1007/978-3-540-71209-1_49.

Comments and questions to:
For website issues: