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.
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.
Clark Barrett, Pascal Fontaine & Cesare Tinelli (2016):
The Satisfiability Modulo Theories Library (SMT-LIB).
Available at http://www.SMT-LIB.org.
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.
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.
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.
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.
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 https://arxiv.org/abs/1505.00672.
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.
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.
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.
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.
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 http://ceur-ws.org/Vol-1889/paper6.pdf.
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.
Wolfgang Schreiner (2019):
The RISC Algorithm Language (RISCAL).
Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria.
Available at https://www.risc.jku.at/research/formal/software/RISCAL.
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 https://www.risc.jku.at/publications/download/risc_6328/21-11.pdf.
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.
SMT-COMP (2021):
SMT-COMP: The International Satisfiability Modulo Theories (SMT) Competition..
Available at https://smt-comp.github.io.
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.
eptcs@eptcs.org