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.
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.
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.
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].
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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].
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.
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.
S.K. Srinivasan (2007):
Efficient Verification of Bit-level Pipelined Machines Using Refinement.
Georgia Institute of Technology.
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.
M. Weiser (1999):
The Computer for the 21st Century.
SIGMOBILE Mob. Comput. Commun. Rev. 3(3),
pp. 3–11,
doi:10.1145/329124.329126.