References

  1. J.-R. Abrial, M. Butler, S. Hallerstede & L. Voisin (2006): An Open Extensible Tool Environment for Event-b. In: 8th Int'l. Conf. Formal Methods and Software Engineering. Springer, pp. 588–605, doi:10.1007/11901433_32.
  2. 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.
  3. 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.
  4. 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].
  5. 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.
  6. 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.
  7. 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.
  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. 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.
  10. R.A. Gamboa (1997): Square Roots in ACL2: A Study in Sonata Form. Technical Report. University of Texas at Austin. Available at http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.57.4803.
  11. 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.
  12. Shant Harutunian (2007): Formal Verification of Computer Controlled Systems. University of Texas, Austin. Available at https://www.lib.utexas.edu/etd/d/2007/harutunians68792/harutunians68792.pdf.
  13. F. Immler (2014): Formally Verified Computation of Enclosures of Solutions of Ordinary Differential Equations. In: NASA Formal Methods, LNCS 8430. Springer, pp. 113–127, doi:10.1007/978-3-319-06200-6_9.
  14. 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.
  15. K. Leino & Rustan M. (2012): Automating Induction with an SMT Solver. In: Verification, Model Checking, and Abstract Interpretation, LNCS 7148. Springer, pp. 315–331, doi:10.1007/978-3-642-27940-9_21.
  16. 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.
  17. 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.
  18. 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.
  19. Y. Peng (2015): Global convergence proof for a digital Phase-Locked Loop. https://bitbucket.org/pennyan/smtlink/src/7fdd38280be9e492a96947019f9b0c8cf10b3d91/examples/DPLL/DPLL_proof.lisp?at=master. [Online; accessed 17-August-2015].
  20. Y. Peng & M. Greenstreet (2015): Integrating SMT with Theorem Proving for Analog/Mixed-Signal Circuit Verification. In: NASA Formal Methods, LNCS 9058. Springer, pp. 310–326, doi:10.1007/978-3-319-17524-9_22.
  21. E. Reeber & W.A. Hunt Jr. (2006): A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA). In: Automated Reasoning, LNCS 4130. Springer, pp. 453–467, doi:10.1007/11814771_38.
  22. S.K. Srinivasan (2007): Efficient Verification of Bit-level Pipelined Machines Using Refinement. Georgia Institute of Technology.
  23. S. Swords & J. Davis (2011): Bit-Blasting ACL2 Theorems. In: 10th Int'l. Workshop on the ACL2 Theorem Prover and its Applications, pp. 84–102, doi:10.4204/EPTCS.70.7.
  24. M. Weiser (1999): The Computer for the 21st Century. SIGMOBILE Mob. Comput. Commun. Rev. 3(3), pp. 3–11, doi:10.1145/329124.329126.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org