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
A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses, Lecture Notes in Computer Science, vol.53, issue.6, pp.135-150, 2011. ,
DOI : 10.1145/1217856.1217859
URL : https://hal.archives-ouvertes.fr/hal-00639130
A Flexible Proof Format for SMT: a Proposal, PxTP 2011: First International Workshop on Proof eXchange for Theorem Proving, pp.15-26, 2011. ,
URL : https://hal.archives-ouvertes.fr/hal-00642544
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, Lecture Notes in Computer Science, vol.144, issue.2, pp.151-156, 2009. ,
DOI : 10.1007/978-3-540-73595-3_38
URL : https://hal.archives-ouvertes.fr/inria-00430634
Symbolic Boolean manipulation with ordered binary-decision diagrams, ACM Computing Surveys, vol.24, issue.3, pp.293-318, 1992. ,
DOI : 10.1145/136035.136043
URL : http://akebono.stanford.edu/users/nanni/courses/EE318/bryant92.pdf
A Short Proof of the Pigeon Hole Principle using Extended Resolution, ACM SIGACT News, vol.8, issue.4, pp.28-32, 1976. ,
On the Lengths of Proofs in the Propositional Calculus (Preliminary Version), STOC, pp.135-148, 1974. ,
Handbook of Tableau Methods, 1999. ,
Quantier Inference Rules for SMT proofs, PxTP 2011: First International Workshop on Proof eXchange for Theorem Proving, pp.33-39, 2011. ,
Synthesis of Fully Testable Circuits From BDDs, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol.23, issue.3, pp.440-443, 2004. ,
DOI : 10.1109/TCAD.2004.823342
An Extensible SAT-solver, Lecture Notes in Computer Science, vol.2919, pp.502-518, 2003. ,
DOI : 10.1007/978-3-540-24605-3_37
BDD circuit optimization for path delay fault testability, Euromicro Symposium on Digital System Design, 2004. DSD 2004., pp.168-172, 2004. ,
DOI : 10.1109/DSD.2004.1333273
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.12.2296
Research Web Page, 2007. ,
Verifying RUP Proofs of Propositional Unsatisfiability, In ISAIM, 2008. ,
Producing and verifying extremely large propositional refutations, Annals of Mathematics and Artificial Intelligence, vol.43, issue.1???4, pp.329-372, 2012. ,
DOI : 10.1007/s10472-012-9322-x
Decision Procedures: an Algorithmic Point of View, 2008. ,
DOI : 10.1007/978-3-662-50497-0
Genetic Algorithm and Variable Neighbourhood Search for BDD Variable Ordering Problem, INFOCOMP Journal of Computer Science, vol.10, issue.1, pp.29-35, 2011. ,
Solving SAT and SAT Modulo Theories, Journal of the ACM, vol.53, issue.6, pp.937-977, 2006. ,
DOI : 10.1145/1217856.1217859
A Generic Tableau Prover and its Integration with Isabelle, J. UCS, vol.5, issue.3, pp.73-87, 1999. ,
Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers, International Workshop on the Implementation of Logics (IWIL-2010), 2010. ,
Isabelle -A Generic Theorem Prover (with a contribution by, Lecture Notes in Computer Science, vol.828, 1994. ,
Extended resolution simulates binary decision diagrams, Discrete Applied Mathematics, vol.156, issue.6, pp.825-837, 2008. ,
DOI : 10.1016/j.dam.2006.11.012
URL : http://doi.org/10.1016/j.dam.2006.11.012
Extended Resolution Proofs for Conjoining BDDs, Lecture Notes in Computer Science, vol.3967, pp.600-611, 2006. ,
DOI : 10.1007/11753728_60
First-Order Logic, 1968. ,
DOI : 10.1201/b10689-23
On the Complexity of Proofs in Propositional Logics, Seminars in Mathematics, pp.466-483, 1970. ,
Abstract, Bulletin of Symbolic Logic, vol.35, issue.04, pp.425-467, 1995. ,
DOI : 10.1145/136035.136043