veriT: An Open, Trustable and Efficient SMT-Solver T Bouton, DCB de Oliveira, D Déharbe, P Fontaine International Conference on Automated Deduction, 151-156, 2009 | 192 | 2009 |
Expressiveness+ automation+ soundness: Towards combining SMT solvers and interactive proof assistants P Fontaine, JY Marion, S Merz, LP Nieto, A Tiu International Conference on Tools and Algorithms for the Construction and …, 2006 | 107 | 2006 |
SMT solvers for Rodin D Déharbe, P Fontaine, Y Guyot, L Voisin International Conference on Abstract State Machines, Alloy, B, VDM, and Z …, 2012 | 64 | 2012 |
Exploiting symmetry in SMT problems D Déharbe, P Fontaine, S Merz, BW Paleo International Conference on Automated Deduction, 222-236, 2011 | 41 | 2011 |
SC2: Satisfiability checking meets symbolic computation E Ábrahám, J Abbott, B Becker, AM Bigatti, M Brain, B Buchberger, ... Intelligent Computer Mathematics: Proceedings CICM 9791, 28-43, 2016 | 38 | 2016 |
Integrating SMT solvers in Rodin D Déharbe, P Fontaine, Y Guyot, L Voisin Science of Computer Programming 94, 130-143, 2014 | 35 | 2014 |
Combinations of theories for decidable fragments of first-order logic P Fontaine International Symposium on Frontiers of Combining Systems, 263-278, 2009 | 30 | 2009 |
Techniques for verification of concurrent systems with invariants P Fontaine PhD thesis, Institut Montefiore, Université de Liege, Belgium, 2004 | 30 | 2004 |
Computing prime implicants D Déharbe, P Fontaine, D Le Berre, B Mazure 2013 Formal Methods in Computer-Aided Design, 46-52, 2013 | 29 | 2013 |
A flexible proof format for SMT: A proposal F Besson, P Fontaine, L Théry | 29 | 2011 |
Compression of propositional resolution proofs via partial regularization P Fontaine, S Merz, BW Paleo International Conference on Automated Deduction, 237-251, 2011 | 28 | 2011 |
Congruence closure with free variables H Barbosa, P Fontaine, A Reynolds International Conference on Tools and Algorithms for the Construction and …, 2017 | 25 | 2017 |
Revisiting enumerative instantiation A Reynolds, H Barbosa, P Fontaine International Conference on Tools and Algorithms for the Construction and …, 2018 | 21 | 2018 |
Quantifier inference rules for SMT proofs D Deharbe, P Fontaine, BW Paleo | 21 | 2011 |
Combining lists with non-stably infinite theories P Fontaine, S Ranise, CG Zarba International Conference on Logic for Programming Artificial Intelligence …, 2005 | 21 | 2005 |
Decidability of invariant validation for paramaterized systems P Fontaine, EP Gribomont International Conference on Tools and Algorithms for the Construction and …, 2003 | 20 | 2003 |
Scalable fine-grained proofs for formula processing H Barbosa, JC Blanchette, M Fleury, P Fontaine Journal of Automated Reasoning 64 (3), 485-510, 2020 | 19 | 2020 |
A gentle non-disjoint combination of satisfiability procedures P Chocron, P Fontaine, C Ringeissen International Joint Conference on Automated Reasoning, 122-136, 2014 | 18 | 2014 |
Combinations of Theories and the Bernays-Schönfinkel-Ramsey Class. P Fontaine VERIFY, 2007 | 17 | 2007 |
Combining non-stably infinite, non-first order theories P Fontaine, P Gribomont Electronic Notes in Theoretical Computer Science 125 (3), 37-51, 2005 | 16 | 2005 |