References

  1. M. Armand, G. Faure, B. Grégoire, C. Keller, L. Théry & B. Werner (2011): A Modular Integration of SAT/SMT Solvers to Coq Through Proof Witnesses. In: 1st Int'l. Conf. Certified Programs and Proofs. Springer, pp. 135–150, doi:10.1007/978-3-642-25379-9_12.
  2. C. Barrett & S. Berezin (2004): CVC Lite: A New Implementation of the Cooperating Validity Checker. In: Computer Aided Verification, LNCS 3114. Springer, pp. 515–518, doi:10.1007/978-3-540-27813-9_49.
  3. C. Barrett, A. Stump & C. Tinelli (2010): The SMT-LIB Standard: Version 2.0. http://www.cs.nyu.edu/~barrett/pubs/BST10.pdf. [Online; accessed 17-August-2015].
  4. F. Besson (2007): Fast Reflexive Arithmetic Tactics the Linear Case and Beyond. In: 2006 Int'l. Conf. Types for Proofs and Programs. Springer, pp. 48–62, doi:10.1007/978-3-540-74464-1_4.
  5. J.C. Blanchette, S. Böhme & L.C. Paulson (2013): Extending Sledgehammer with SMT Solvers. J. Automated Reasoning 51(1), pp. 109–128, doi:10.1007/s10817-013-9278-5.
  6. D. Déharbe, P. Fontaine, Y. Guyot & L. Voisin (2014): Integrating SMT Solvers in Rodin. Sci. Comput. Program. 94(P2), pp. 130–143, doi:10.1016/j.scico.2014.04.012.
  7. David L. Dill (1987): Trace Theory for Automatic Hierarchical Verification of Speed-independent Circuits. Carnegie Mellon University, Pittsburgh, PA, USA. Available at http://reports-archive.adm.cs.cmu.edu/anon/scan/CMU-CS-88-119.pdf. AAI8814716.
  8. B. Dutertre (2014): Yices 2.2. In: Computer Aided Verification, LNCS 8559. Springer, pp. 737–744, doi:10.1007/978-3-319-08867-9_49.
  9. Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds & Clark Barrett (2017): SMTCoq: A Plug-In for Integrating SMT Solvers into Coq. In: Rupak Majumdar & Viktor Kunčak: Computer Aided Verification. Springer International Publishing, Cham, pp. 126–133, doi:10.1007/978-3-319-63390-9_7.
  10. Levent Erkök & John Matthews (2008): Using Yices as an Automated Solver in Isabelle/HOL. In: In Automated Formal Methods’08. ACM Press, pp. 3–13. Available at http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.156.8123.
  11. P. Fontaine, J.-Y. Marion, S. Merz, L.P. Nieto & A. Tiu (2006): Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants. In: 12th Int'l. Conf. Tools and Algorithms for the Construction and Analysis of Systems. Springer, pp. 167–181, doi:10.1007/11691372_11.
  12. J. Harrison & L. Théry (1998): A Skeptic's Approach to Combining HOL and Maple. J. Automated Reasoning 21(3), pp. 279–294, doi:10.1023/A:1006023127567.
  13. Marijn Heule, Warren Hunt, Matt Kaufmann & Nathan Wetzler (2017): Efficient, Verified Checking of Propositional Proofs. In: Mauricio Ayala-Rincón & César A. Muñoz: Interactive Theorem Proving. Springer International Publishing, Cham, pp. 269–284, doi:10.1007/978-3-319-66107-0_18.
  14. L. Paulson J. Blanchette (2017): Sledgehammer. https://isabelle.in.tum.de/dist/doc/sledgehammer.pdf. [Online; accessed 14-July-2018].
  15. Matt Kaufmann & Sol Swords (2017): Meta-extract: Using Existing Facts in Meta-reasoning. In: Slobodová & Jr., pp. 47–60, doi:10.4204/EPTCS.249.4. Available at http://arxiv.org/abs/1705.00766.
  16. S.K. Lahiri & S.A. Seshia (2004): The UCLID Decision Procedure. In: Computer Aided Verification, LNCS 3114. Springer, pp. 475–478, doi:10.1007/978-3-540-27813-9_40.
  17. P. Manolios & S.K. Srinivasan (2006): A Framework for Verifying Bit-Level Pipelined Machines Based on Automated Deduction and Decision Procedures. J. of Automated Reasoning 37(1-2), pp. 93–116, doi:10.1007/s10817-006-9035-0.
  18. S. Mclaughlin, Cl. Barrett & Y. Ge (2006): Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite. In: In Proc. 3rd Workshop on Pragmatics of Decision Procedures in Automated Reasoning, ENTCS 144(2). Elsevier, pp. 43–51, doi:10.1016/j.entcs.2005.12.005.
  19. S. Merz & H. Vanzetto (2012): Automatic Verification of TLA^+; Proof Obligations with SMT Solvers. In: 18th Int'l. Conf. Logic for Programming, Artificial Intelligence, and Reasoning. Springer, pp. 289–303, doi:10.1007/978-3-642-28717-6_23.
  20. Leonardo Moura & Nikolaj Bjørner (2008): Z3: An Efficient SMT Solver. In: C.R. Ramakrishnan & Jakob Rehof: Tools and Algorithms for the Construction and Analysis of Systems, Lecture Notes in Computer Science 4963. Springer Berlin Heidelberg, pp. 337–340, doi:10.1007/978-3-540-78800-3_24.
  21. Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn & Jakob von Raumer (2015): The Lean Theorem Prover (System Description). In: Amy P. Felty & Aart Middeldorp: Automated Deduction - CADE-25. Springer International Publishing, pp. 378–388, doi:10.1007/978-3-319-21401-6_26.
  22. Yan Peng & Mark Greenstreet (2015): Extending ACL2 with SMT Solvers. In: Matt Kaufmann & David L. Rager: Proceedings Thirteenth International Workshop on the ACL2 Theorem Prover and Its Applications, Electronic Proceedings in Theoretical Computer Science 192. Open Publishing Association, Austin, Texas, USA, 1–2 October 2015, pp. 61–77, doi:10.4204/EPTCS.192.6.
  23. Yan Peng & Mark Greenstreet (2015): Integrating SMT with Theorem Proving for Analog/Mixed-Signal Circuit Verification. In: Klaus Havelund, Gerard Holzmann & Rajeev Joshi: NASA Formal Methods. Springer International Publishing, pp. 310–326, doi:10.1007/978-3-319-17524-9_22.
  24. Anna Slobodová & Warren A. Hunt Jr. (2017): Proceedings 14th International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, May 22-23, 2017. EPTCS 249. Available at http://arxiv.org/abs/1705.00766.
  25. S.K. Srinivasan (2007): Efficient Verification of Bit-level Pipelined Machines Using Refinement. Georgia Institute of Technology. Available at http://hdl.handle.net/1853/19815.
  26. Niki Vazou, Anish Tondwalkar, Vikraman Choudhury, Ryan G. Scott, Ryan R. Newton, Philip Wadler & Ranjit Jhala (2017): Refinement Reflection: Complete Verification with SMT. Proc. ACM Program. Lang. 2(POPL), pp. 53:1–53:31, doi:10.1145/3158141.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org