, Symbolic Model Checking without BDDs, TACAS'99, pp.193-207, 1999.
DOI : 10.1007/3-540-49059-0_14
, Embedding Deduction Modulo into a Prover, CSL 2010, pp.155-169, 2010.
DOI : 10.1007/978-3-642-15205-4_15
, Experimenting with Deduction Modulo, Lecture Notes in Artificial Intelligence, vol.43, issue.4, pp.162-176, 2011.
DOI : 10.1007/978-3-642-02959-2_10
URL : https://hal.archives-ouvertes.fr/hal-01125858
, Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo, LPAR-19, pp.274-290, 2013.
DOI : 10.1007/978-3-642-45221-5_20
URL : https://hal.archives-ouvertes.fr/hal-00909784
, Polarized Resolution Modulo, TCS 2010, pp.182-196, 2010.
DOI : 10.1007/978-3-642-15240-5_14
URL : https://hal.archives-ouvertes.fr/hal-01054460
, Theorem Proving Modulo, Journal of Automated Reasoning, vol.31, issue.1, pp.33-72, 2003.
DOI : 10.1023/A:1027357912519
URL : https://hal.archives-ouvertes.fr/hal-01199506
, A Logical Approach to CTL, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00919467
, Axiomatizing Truth in a Finite Model (2013), https://who.rocq.inria.fr/ Gilles
, CTL Model Checking in Deduction Modulo (2015), https
, iProver ??? An Instantiation-Based Theorem Prover for First-Order Logic (System Description), IJCAR 2008, pp.292-298, 2008.
DOI : 10.1007/978-3-540-71070-7_24
, An integration of model checking with automated proof checking, CAV 1995, pp.84-97, 1995.
DOI : 10.1007/3-540-60045-0_42
, Basic Proof Theory, 1996.
DOI : 10.1017/CBO9781139168717
, Bounded Semantics of CTL and SAT-Based Verification, ICFEM 2009, pp.286-305, 2009.
DOI : 10.1007/978-3-642-10373-5_15
, QBF Encoding of Temporal Properties and QBF-Based Verification, IJCAR 2014, pp.224-239, 2014.
DOI : 10.1007/978-3-319-08587-6_16