| [4] | Michaël Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Théry and Benjamin Werner. Une intégration des solveurs SMT dans l'assistant de preuve Coq à base de certificats. In Journées GDR - GPL - CIEL 2012, Rennes, Juin 2012. |
| [3] | Michael Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Théry, and Benjamin Werner. A modular integration of SAT/SMT solvers to coq through proof witnesses. In First International Conference on Certified Programs and Proofs, Tawain, December 7-9, Lecture Notes in Computer Science. Springer, 2011. |
| [2] | Michaël Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Théry and Benjamin Wener. Verifying SAT and SMT in Coq for a fully automated decision procedure. In PSATTT'11: International Workshop on Proof-Search in Axiomatic Theories and Type Theories, Aug 2011, Wroclaw, Poland. |
| [1] | Michaël Armand, Benjamin Grégoire, Arnaud Spiwack, and Laurent Théry. Extending coq with imperative features and its application to SAT verication. In Interactive Theorem Proving, international Conference, ITP 2010, Edinburgh, Scotland, July 11-14, 2010, Proceedings, Lecture Notes in Computer Science. Springer, 2010. |