- Frédéric Besson, Thomas Jensen, David Pichardie, Tiphaine Turpin. Certified Result Checking for Polyhedral Analysis of Bytecode Programs. Trustworthy Global Computing 2010.
- Frédéric Besson. On using an inexact floating-point LP solver for deciding linear arithmetic in an SMT solver. SMT Workshop 2010.
- Michaël Armand, Benjamin Grégoire, Arnaud Spiwack and Laurent Théry,
Extending Coq with Imperative Features and its Application to SAT Verification, ITP'10,
FLoC, Edinburgh, 2010.
- David Déharbe. Automatic Verification for a Class of Proof Obligations with SMT-Solvers, 217-230. In Abstract State Machines, Alloy, B and Z, Second International Conference, ABZ 2010, Orford, QC, Canada, February 22-25, 2010. Proceedings.
- Pascal Fontaine, Stephan Merz and Bruno Woltzenlogel Paleo.
Exploring and Exploiting Algebraic and Graphical Properties of
Resolution, In Aarti Gupta and Daniel Kroening editors In
Proc. Workshop on Satisfiability Modulo Theories (SMT), 2010.
- Thomas Bouton, Diego Caminha B. de Oliveira, David Déharbe
and Pascal Fontaine. GridTPT: a distributed platform for Theorem
Prover Testing, In Boris Konev, Renate Schmidt and Stephan Schulz,
editors, In Proc. Workshop on Practical Aspects of Automated
Reasoning 2010.
- Pascal Fontaine. Combinations of theories for decidable fragments
of first-order logic. In Silvio Ghilardi and Roberto
Sebastiani, editors, In Proc. Frontiers of Combining Systems
(FroCoS), Trento, volume 5749 of LNCS, pages
263--278. Springer-Verlag, 2009.
- Thomas Bouton, Diego Caminha B. de Oliveira, David Déharbe and
Pascal Fontaine. veriT: an open, trustable and efficient SMT-solver.
In Renate A. Schmidt, editor, In Proc. Conference on Automated
Deduction (CADE), volume 5663 of LNCS, pages
151--156. Springer-Verlag, 2009.
- Jean-François Couchot, Alain Giorgetti and Nicolas Stouls. Graph Based Reduction
of Program Veri cation Conditions. In Hassen Saïdi and N. Shankar, editors,
In Proc. Workshop on Automated Formal Methods (AFM'09, colocated with CAV'09),
pages 40--47, Grenoble, France. ACM Press, 2009.
- Enrica Nicolini, Christophe Ringeissen and Michaël Rusinowitch. Satisfiability Procedures for Combination of Theories Sharing Integer Offsets. In Stefan Kowalewski and Anna Philippou, editors, In Proc. Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 5505 of LNCS, pages 428--442. Springer-Verlag, 2009.
- Enrica Nicolini, Christophe Ringeissen and Michaël Rusinowitch. Combinable Extensions of Abelian Groups. In Renate A. Schmidt, editor, In Proc. Conference on Automated Deduction (CADE), volume 5663 of LNCS, pages 51--66. Springer-Verlag, 2009.
- Enrica Nicolini, Christophe Ringeissen and Michaël Rusinowitch. Data Structures with Arithmetic Constraints: A Non-disjoint Combination. In Silvio Ghilardi and Roberto Sebastiani, editors, In Proc. Frontiers of Combining Systems (FroCoS), Trento, volume 5749 of LNCS, pages 319--334. Springer-Verlag, 2009.