The B-Book: Assigning Programs to Meanings, 1996. ,
DOI : 10.1017/CBO9780511624162
Autarkic Computations in Formal Proofs, Journal of Automated Reasoning, vol.28, issue.3, pp.321-336, 2002. ,
DOI : 10.1023/A:1015761529444
Hierarchic Superposition with Weak Abstraction, Conference on Automated Deduction, pp.39-57, 2013. ,
DOI : 10.1007/978-3-642-38574-2_3
URL : https://hal.archives-ouvertes.fr/hal-00931919
Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs, In Logic for Programming Artificial Intelligence and Reasoning LNCS/LNAI, vol.4790, pp.151-165, 2007. ,
DOI : 10.1007/978-3-540-75560-9_13
URL : https://hal.archives-ouvertes.fr/inria-00315920
Z3: An Efficient SMT Solver, Tools and Algorithms for the Construction and Analysis of Systems (TACAS), pp.337-340, 2008. ,
DOI : 10.1007/978-3-540-78800-3_24
Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), pp.274-290, 2013. ,
DOI : 10.1007/978-3-642-45221-5_20
URL : https://hal.archives-ouvertes.fr/hal-00909784
The BWare Project: Building a Proof Platform for the Automated Verification of B Proof Obligations, Abstract State Machines, Alloy, B, VDM, and Z (ABZ), Lecture Notes in Computer Science (LNCS), pp.126-127, 2014. ,
DOI : 10.1007/978-3-662-43652-3_26
URL : https://hal.archives-ouvertes.fr/hal-00998092
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
Integrating Simplex with DPLL(T), 2006. ,
An Algorithm for Integer Solutions to Linear Problems, Recent Advances in Mathematical Programming, pp.269-302, 1963. ,
Decision Procedures: An Algorithmic Point of View. Texts in Theoretical Computer Science. An EATCS Series, 2008. ,
DOI : 10.1007/978-3-662-50497-0
Integer and Combinatorial Optimization. Wiley-Interscience Series in Discrete Mathematics and Optimization, 1999. ,
DOI : 10.1002/9781118627372
URL : http://dx.doi.org/10.1016/s0898-1221(99)91259-2
A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic, Logic for Programming, pp.274-289, 2008. ,
DOI : 10.1007/978-3-540-89439-1_20
The TPTP Problem Library and Associated Infrastructure, Journal of Automated Reasoning, vol.13, issue.2, pp.337-362, 2009. ,
DOI : 10.1007/s10817-009-9143-8