Follow
Pascal Fontaine
Title
Cited by
Cited by
Year
veriT: An Open, Trustable and Efficient SMT-Solver
T Bouton, D Caminha B. de Oliveira, D Déharbe, P Fontaine
Automated Deduction–CADE-22: 22nd International Conference on Automated …, 2009
2382009
Expressiveness+ automation+ soundness: Towards combining SMT solvers and interactive proof assistants
P Fontaine, JY Marion, S Merz, LP Nieto, A Tiu
Tools and Algorithms for the Construction and Analysis of Systems: 12th …, 2006
1172006
SMT solvers for Rodin
D Déharbe, P Fontaine, Y Guyot, L Voisin
Abstract State Machines, Alloy, B, VDM, and Z: Third International …, 2012
712012
Revisiting enumerative instantiation
A Reynolds, H Barbosa, P Fontaine
Tools and Algorithms for the Construction and Analysis of Systems: 24th …, 2018
532018
Exploiting Symmetry in SMT Problems.
D Déharbe, P Fontaine, S Merz, BW Paleo
CADE 6803, 222-236, 2011
522011
: Satisfiability Checking Meets Symbolic Computation: (Project Paper)
E Ábrahám, J Abbott, B Becker, AM Bigatti, M Brain, B Buchberger, ...
Intelligent Computer Mathematics: 9th International Conference, CICM 2016 …, 2016
492016
Congruence closure with free variables
H Barbosa, P Fontaine, A Reynolds
Tools and Algorithms for the Construction and Analysis of Systems: 23rd …, 2017
432017
Integrating SMT solvers in Rodin
D Déharbe, P Fontaine, Y Guyot, L Voisin
Science of Computer Programming 94, 130-143, 2014
422014
Computing prime implicants
D Déharbe, P Fontaine, D Le Berre, B Mazure
2013 Formal Methods in Computer-Aided Design, 46-52, 2013
362013
Scalable fine-grained proofs for formula processing
H Barbosa, JC Blanchette, M Fleury, P Fontaine
Journal of Automated Reasoning 64 (3), 485-510, 2020
352020
Compression of propositional resolution proofs via partial regularization
P Fontaine, S Merz, B Woltzenlogel Paleo
Automated Deduction–CADE-23: 23rd International Conference on Automated …, 2011
342011
Combinations of theories for decidable fragments of first-order logic
P Fontaine
Frontiers of Combining Systems: 7th International Symposium, FroCoS 2009 …, 2009
342009
A flexible proof format for SMT: A proposal
F Besson, P Fontaine, L Théry
First International Workshop on Proof eXchange for Theorem Proving-PxTP 2011, 2011
332011
Proofs in satisfiability modulo theories
C Barrett, L De Moura, P Fontaine
All about proofs, Proofs for all 55 (1), 23-44, 2015
312015
Techniques for verification of concurrent systems with invariants
P Fontaine
PhD thesis, Institut Montefiore, Université de Liege, Belgium, 2004
292004
Quantifier inference rules for SMT proofs
D Déharbe, P Fontaine, BW Paleo
First International Workshop on Proof eXchange for Theorem Proving-PxTP 2011, 2011
262011
Subtropical satisfiability
P Fontaine, M Ogawa, T Sturm, XT Vu
Frontiers of Combining Systems: 11th International Symposium, FroCoS 2017 …, 2017
222017
Combining lists with non-stably infinite theories
P Fontaine, S Ranise, CG Zarba
Logic for Programming, Artificial Intelligence, and Reasoning: 11th …, 2005
222005
A gentle non-disjoint combination of satisfiability procedures
P Chocron, P Fontaine, C Ringeissen
Automated Reasoning: 7th International Joint Conference, IJCAR 2014, Held as …, 2014
212014
Decidability of invariant validation for paramaterized systems
P Fontaine, EP Gribomont
TACAS 3 (2619), 97-112, 2003
202003
The system can't perform the operation now. Try again later.
Articles 1–20