J. Abrial, The B-Book: Assigning Programs to Meanings, 1996.
DOI : 10.1017/CBO9780511624162

H. Barendregt and E. Barendsen, Autarkic Computations in Formal Proofs, Journal of Automated Reasoning, vol.28, issue.3, pp.321-336, 2002.
DOI : 10.1023/A:1015761529444

P. Baumgartner and U. Waldmann, 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

R. Bonichon, D. Delahaye, and D. Doligez, 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

L. M. De-moura and N. Bjørner, 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

D. Delahaye, D. Doligez, F. Gilbert, P. Halmagrand, and O. Hermant, 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

D. Delahaye, C. Dubois, C. Marché, and D. Mentré, 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

G. Dowek, T. Hardin, and C. Kirchner, 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

B. Dutertre and L. M. De-moura, Integrating Simplex with DPLL(T), 2006.

R. E. Gomory, An Algorithm for Integer Solutions to Linear Problems, Recent Advances in Mathematical Programming, pp.269-302, 1963.

D. Kroening and O. Strichman, Decision Procedures: An Algorithmic Point of View. Texts in Theoretical Computer Science. An EATCS Series, 2008.
DOI : 10.1007/978-3-662-50497-0

G. L. Nemhauser and L. A. Wolsey, 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

P. Rümmer, 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

G. Sutcliffe, 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