概述

1. Handbook of Model Checking(Chapter 11) 2018
2. Handbook of Practical Logic and Automated Reasoning(Chapter 4, 5) Harrison, John 2009
3. Decision Procedures - An Algorithmic Point of View, Second Edition Kroening, Daniel, and Strichman, Ofer 2016

基本算法

1. JACM

   Simplify: a theorem prover for program checking Detlefs, David, Nelson, Greg, and Saxe, James B. J. ACM 2005
2. JACM

   Solving SAT and SAT Modulo Theories: From an abstract Davis–Putnam–Logemann–Loveland procedure to DPLL(T) Nieuwenhuis, Robert, Oliveras, Albert, and Tinelli, Cesare J. ACM 2006
3. IJCAR

   Engineering DPLL(T) + Saturation Moura, Leonardo Mendonça, and Bjørner, Nikolaj In Automated Reasoning, 4th International Joint Conference, IJCAR 2008, Sydney, Australia, August 12-15, 2008, Proceedings 2008
4. JAR

   Adding Decision Procedures to SMT Solvers Using Axioms with Triggers Dross, Claire, Conchon, Sylvain, Kanig, Johannes, and Paskevich, Andrei J. Autom. Reason. 2016

Congruence Closure

1. Inf. Comput.

   Fast congruence closure and extensions Nieuwenhuis, Robert, and Oliveras, Albert Inf. Comput. 2007
2. CADE

   Efficient E-Matching for SMT Solvers Moura, Leonardo Mendonça, and Bjørner, Nikolaj In Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings 2007
3. TACAS

   Congruence Closure with Free Variables Barbosa, Haniel, Fontaine, Pascal, and Reynolds, Andrew In Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part II 2017

理论判定算法

1. CAV

   A Fast Linear-Arithmetic Solver for DPLL(T) Dutertre, Bruno, and Moura, Leonardo Mendonça In Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings 2006
2. VMCAI

   What’s Decidable About Arrays? Bradley, Aaron R., Manna, Zohar, and Sipma, Henny B. In Verification, Model Checking, and Abstract Interpretation, 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceedings 2006
3. FMCAD

   Generalized, efficient array decision procedures Moura, Leonardo Mendonça, and Bjørner, Nikolaj In Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2009, 15-18 November 2009, Austin, Texas, USA 2009

量词实例化

1. CAV

   Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories Ge, Yeting, and Moura, Leonardo Mendonça In Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings 2009
2. CAV

   Finite Model Finding in SMT Reynolds, Andrew, Tinelli, Cesare, Goel, Amit, and Krstic, Sava In Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings 2013
3. CAV

   Counterexample-Guided Quantifier Instantiation for Synthesis in SMT Reynolds, Andrew, Deters, Morgan, Kuncak, Viktor, Tinelli, Cesare, and Barrett, Clark W. In Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II 2015
4. FMSD

   Solving quantified linear arithmetic by counterexample-guided instantiation Reynolds, Andrew, King, Tim, and Kuncak, Viktor Formal Methods Syst. Des. 2017
5. CAV

   Solving Quantified Bit-Vectors Using Invertibility Conditions Niemetz, Aina, Preiner, Mathias, Reynolds, Andrew, Barrett, Clark W., and Tinelli, Cesare In Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part II 2018
6. FMCAD

   Fair and Adventurous Enumeration of Quantifier Instantiations Janota, Mikolás, Barbosa, Haniel, Fontaine, Pascal, and Reynolds, Andrew In Formal Methods in Computer Aided Design, FMCAD 2021, New Haven, CT, USA, October 19-22, 2021 2021
7. TACAS

   Syntax-Guided Quantifier Instantiation Niemetz, Aina, Preiner, Mathias, Reynolds, Andrew, Barrett, Clark W., and Tinelli, Cesare In Tools and Algorithms for the Construction and Analysis of Systems - 27th International Conference, TACAS 2021, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2021, Luxembourg City, Luxembourg, March 27 - April 1, 2021, Proceedings, Part II 2021
8. TACAS

   Revisiting Enumerative Instantiation Reynolds, Andrew, Barbosa, Haniel, and Fontaine, Pascal In Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Part II 2018
9. CADE

   Quantifier Instantiation Techniques for Finite Model Finding in SMT Reynolds, Andrew, Tinelli, Cesare, Goel, Amit, Krstic, Sava, Deters, Morgan, and Barrett, Clark W. In Automated Deduction - CADE-24 - 24th International Conference on Automated Deduction, Lake Placid, NY, USA, June 9-14, 2013. Proceedings 2013

系统介绍

1. CAV

   Z3: An Efficient SMT Solver Moura, Leonardo Mendonça, and Bjørner, Nikolaj In Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS 2008, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Budapest, Hungary, March 29-April 6, 2008. Proceedings 2008
2. CADE

   veriT: An Open, Trustable and Efficient SMT-Solver Bouton, Thomas, Oliveira, Diego Caminha Barbosa De, Déharbe, David, and Fontaine, Pascal In Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings 2009
3. CAV

   CVC4 Barrett, Clark W., Conway, Christopher L., Deters, Morgan, Hadarean, Liana, Jovanovic, Dejan, King, Tim, Reynolds, Andrew, and Tinelli, Cesare In Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings 2011
4. SAT

   SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving Corzilius, Florian, Kremer, Gereon, Junges, Sebastian, Schupp, Stefan, and Ábrahám, Erika In Theory and Applications of Satisfiability Testing - SAT 2015 - 18th International Conference, Austin, TX, USA, September 24-27, 2015, Proceedings 2015

程序验证工具

1. LPAR

   Dafny: An Automatic Program Verifier for Functional Correctness Leino, K. Rustan M. In Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Dakar, Senegal, April 25-May 1, 2010, Revised Selected Papers 2010
2. ESOP

   Why3 - Where Programs Meet Provers Filliâtre, Jean-Christophe, and Paskevich, Andrei In Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings 2013

证明重构

1. CADE

   Sledgehammer: Judgement Day Böhme, Sascha, and Nipkow, Tobias In Automated Reasoning, 5th International Joint Conference, IJCAR 2010, Edinburgh, UK, July 16-19, 2010. Proceedings 2010
2. ITP

   Fast LCF-Style Proof Reconstruction for Z3 Böhme, Sascha, and Weber, Tjark In Interactive Theorem Proving, First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings 2010
3. CPP

   A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses Armand, Michaël, Faure, Germain, Grégoire, Benjamin, Keller, Chantal, Théry, Laurent, and Werner, Benjamin In Certified Programs and Proofs - First International Conference, CPP 2011, Kenting, Taiwan, December 7-9, 2011. Proceedings 2011
4. CADE

   Extending Sledgehammer with SMT Solvers Blanchette, Jasmin Christian, Böhme, Sascha, and Paulson, Lawrence C. In Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31 - August 5, 2011. Proceedings 2011
5. FMSD

   SMT proof checking using a logical framework Stump, Aaron, Oe, Duckki, Reynolds, Andrew, Hadarean, Liana, and Tinelli, Cesare Formal Methods Syst. Des. 2013
6. JFR

   Hammering towards QED Blanchette, Jasmin Christian, Kaliszyk, Cezary, Paulson, Lawrence C., and Urban, Josef J. Formaliz. Reason. 2016

其它

1. JACM

   Proving the Incompatibility of Efficiency and Strategyproofness via SMT Solving Brandl, Florian, Brandt, Felix, Eberl, Manuel, and Geist, Christian J. ACM 2018