The semantics of reflected proof, [1990] Proceedings. Fifth Annual IEEE Symposium on Logic in Computer Science, pp.95-105, 1990. ,
DOI : 10.1109/LICS.1990.113737
Extending Coq with Imperative Features and Its Application to SAT Verification, pp.83-98 ,
DOI : 10.1007/978-3-642-14052-5_8
URL : https://hal.archives-ouvertes.fr/inria-00502496
Combining the Coq proof assistant with first-order decision procedures, 2006. ,
The Static Driver Verifier Research Platform, CAV. LNCS, pp.119-122, 2010. ,
DOI : 10.1007/978-3-642-14295-6_11
Boogie: A Modular Reusable Verifier for Object-Oriented Programs, FMCO. LNCS, pp.364-387, 2005. ,
DOI : 10.1007/11804192_17
Interactive Theorem Proving and Program Development, Coq'Art: The Calculus of Inductive Constructions, 2004. ,
URL : https://hal.archives-ouvertes.fr/hal-00344237
Fast Reflexive Arithmetic Tactics the Linear Case and Beyond, TYPES. LNCS, pp.48-62, 2006. ,
DOI : 10.1007/978-3-540-74464-1_4
Fast LCF-Style Proof Reconstruction for Z3, pp.179-194 ,
DOI : 10.1007/978-3-642-14052-5_14
veriT: An Open, Trustable and Efficient SMT-Solver, CADE. LNCS, pp.151-156, 2009. ,
DOI : 10.1007/978-3-540-73595-3_38
URL : https://hal.archives-ouvertes.fr/inria-00430634
Ergo : a theorem prover for polymorphic first-order logic modulo theories, 2006. ,
A machine program for theorem-proving, Communications of the ACM, vol.5, issue.7, pp.394-397, 1962. ,
DOI : 10.1145/368273.368557
A Computing Procedure for Quantification Theory, Journal of the ACM, vol.7, issue.3, pp.201-215, 1960. ,
DOI : 10.1145/321033.321034
Simplify: a theorem prover for program checking, Journal of the ACM, vol.52, issue.3, pp.365-473, 2005. ,
DOI : 10.1145/1066100.1066102
The Yices SMT Solver, Tech. rep., SRI, 2006. ,
An Extensible SAT-solver, SAT. LNCS, pp.502-518, 2003. ,
Type-safe modular hash-consing, Proceedings of the 2006 workshop on ML , ML '06, pp.12-19, 2006. ,
DOI : 10.1145/1159876.1159880
The Why/Krakatoa/Caduceus Platform for Deductive Program Verification, CAV. LNCS, pp.173-177, 2007. ,
DOI : 10.1007/978-3-540-73368-3_21
Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants, TACAS. LNCS, pp.167-181, 2006. ,
DOI : 10.1007/3-540-45620-1_26
URL : https://hal.archives-ouvertes.fr/inria-00001088
A History of Satisfiability, Handbook of Satisfiability, pp.3-74, 2009. ,
A computer-checked proof of the four colour theorem, Tech. rep., Microsoft Research Cambridge, 2005. ,
A compiled implementation of strong reduction, pp.235-246, 2002. ,
A Computational Approach to Pocklington Certificates in Type Theory, FLOPS. LNCS, pp.97-113, 2006. ,
DOI : 10.1007/11737414_8
Formal Proof ? Theory and Practice, Notices of the American Mathematical Society, vol.55, 2008. ,
Certified Computer Algebra on Top of an Interactive Theorem Prover, Calculemus/MKM, pp.94-105, 2007. ,
DOI : 10.1007/978-3-540-73086-6_8
Interactive Theorem Proving, Proceedings, Lecture Notes in Computer Science, vol.6172, 2010. ,
DOI : 10.1007/978-3-642-14052-5
Dsolve: Safety Verification via Liquid Types, CAV. LNCS, pp.123-126, 2010. ,
DOI : 10.1007/978-3-642-14295-6_12
Formal verification of a realistic compiler, Communications of the ACM, vol.52, issue.7, pp.107-115, 2009. ,
DOI : 10.1145/1538788.1538814
URL : https://hal.archives-ouvertes.fr/inria-00415861
Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme, FroCos. LNCS, pp.287-303, 2009. ,
DOI : 10.1016/j.jal.2007.07.003
Practical applications of Boolean Satisfiability, 2008 9th International Workshop on Discrete Event Systems, 2008. ,
DOI : 10.1109/WODES.2008.4605925
Cooperating Theorem Provers: A Case Study Combining HOL-Light and CVC Lite, Electronic Notes in Theoretical Computer Science, vol.144, issue.2, pp.43-51, 2006. ,
DOI : 10.1016/j.entcs.2005.12.005
Z3: An Efficient SMT Solver, TACAS. LNCS, pp.337-340, 2008. ,
DOI : 10.1007/978-3-540-78800-3_24
Simplification by Cooperating Decision Procedures, ACM Transactions on Programming Languages and Systems, vol.1, issue.2, pp.245-257, 1979. ,
DOI : 10.1145/357073.357079
Solving SAT and SAT Modulo Theories, Journal of the ACM, vol.53, issue.6, pp.937-977, 2006. ,
DOI : 10.1145/1217856.1217859
Pex???White Box Test Generation for .NET, TAP. LNCS, pp.134-153, 2008. ,
DOI : 10.1007/978-3-540-79124-9_10
SAT-based Finite Model Generation for Higher-Order Logic, 2008. ,