A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses, CPP 2011, vol.7086, pp.135-150, 2011. ,
URL : https://hal.archives-ouvertes.fr/hal-00639130
Scalable Fine-Grained Proofs for Formula Processing, Journal of Automated Reasoning, 2019. ,
URL : https://hal.archives-ouvertes.fr/hal-01526841
Better SMT proofs for easier reconstruction, 2019. ,
, The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org, 2016.
Satisfiability Modulo Theories, Handbook of Satisfiability, vol.26, pp.825-885, 2009. ,
URL : https://hal.archives-ouvertes.fr/hal-01095009
, A Flexible Proof Format for SMT: A Proposal, pp.15-26, 2011.
Semi-intelligible Isar Proofs from Machine-Generated Proofs, Journal of Automated Reasoning, vol.56, issue.2, pp.155-200, 2016. ,
Fast LCF-Style Proof Reconstruction for Z3, ITP 2010, vol.6172, pp.179-194, 2010. ,
veriT: An Open, Trustable and Efficient SMT-solver, CADE 2009, vol.5663, pp.151-156, 2009. ,
URL : https://hal.archives-ouvertes.fr/inria-00430634
Verified construction of static single assignment form, CC, ACM, pp.67-76, 2016. ,
Quantifier Inference Rules for SMT Proofs, pp.33-39, 2011. ,
Extending SMTCoq, a Certified Checker for SMT (Extended Abstract), EPTCS, vol.210, pp.21-29, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01388984
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. ,
, Z3: An Efficient SMT Solver, TACAS 2008, vol.4963, pp.337-340, 2008.
Formalization of Bachmair and Ganzinger's Ordered Resolution Prover. Archive of Formal Proofs, Dmitriy Traytel & Uwe Waldmann, 2018. ,
Formalizing Bachmair and Ganzinger's Ordered Resolution Prover, IJCAR, LNCS 10900, pp.89-107, 2018. ,
, Theory of Linear and Integer Programming. Wiley -Interscience Series in Discrete Mathematics and Optimization, 1999.
SMT Proof Checking Using a Logical Framework, Liana Hadarean & Cesare Tinelli, vol.42, issue.1, pp.91-118, 2013. ,
Verified Construction of Static Single Assignment Form. Archive of Formal Proofs, 2016. ,