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