| veriT: an open, trustable and efficient SMT-solver T Bouton, D Caminha B. de Oliveira, D Déharbe, P Fontaine International Conference on Automated Deduction, 151-156, 2009 | 264 | 2009 |
| 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 | 123 | 2006 |
| Revisiting enumerative instantiation A Reynolds, H Barbosa, P Fontaine Tools and Algorithms for the Construction and Analysis of Systems: 24th …, 2018 | 78 | 2018 |
| 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 | 76 | 2012 |
| Exploiting symmetry in SMT problems D Déharbe, P Fontaine, S Merz, B Woltzenlogel Paleo International Conference on Automated Deduction, 222-236, 2011 | 62 | 2011 |
| : Satisfiability Checking Meets Symbolic Computation: (Project Paper) E Ábrahám, J Abbott, B Becker, AM Bigatti, M Brain, B Buchberger, ... International Conference on Intelligent Computer Mathematics, 28-43, 2016 | 55 | 2016 |
| Congruence closure with free variables H Barbosa, P Fontaine, A Reynolds International Conference on Tools and Algorithms for the Construction and …, 2017 | 49 | 2017 |
| Integrating SMT solvers in Rodin D Déharbe, P Fontaine, Y Guyot, L Voisin Science of Computer Programming 94, 130-143, 2014 | 49 | 2014 |
| Scalable fine-grained proofs for formula processing H Barbosa, JC Blanchette, M Fleury, P Fontaine Journal of Automated Reasoning 64 (3), 485-510, 2020 | 45 | 2020 |
| Computing prime implicants D Déharbe, P Fontaine, D Le Berre, B Mazure 2013 Formal Methods in Computer-Aided Design, 46-52, 2013 | 45 | 2013 |
| Proofs in satisfiability modulo theories C Barrett, L De Moura, P Fontaine All about proofs, Proofs for all 55 (1), 23-44, 2015 | 40 | 2015 |
| Combinations of theories for decidable fragments of first-order logic P Fontaine International Symposium on Frontiers of Combining Systems, 263-278, 2009 | 40 | 2009 |
| 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 | 37 | 2011 |
| 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 | 35 | 2011 |
| Subtropical satisfiability P Fontaine, M Ogawa, T Sturm, XT Vu International Symposium on Frontiers of Combining Systems, 189-206, 2017 | 31 | 2017 |
| Techniques for verification of concurrent systems with invariants P Fontaine PhD thesis, Institut Montefiore, Université de Liege, Belgium, 2004 | 29 | 2004 |
| 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 | 25 | 2011 |
| Combining lists with non-stably infinite theories P Fontaine, S Ranise, CG Zarba Logic for Programming, Artificial Intelligence, and Reasoning: 11th …, 2005 | 22 | 2005 |
| A gentle non-disjoint combination of satisfiability procedures P Chocron, P Fontaine, C Ringeissen International Joint Conference on Automated Reasoning, 122-136, 2014 | 21 | 2014 |
| Decidability of invariant validation for paramaterized systems P Fontaine, EP Gribomont International Conference on Tools and Algorithms for the Construction and …, 2003 | 20 | 2003 |
David DeharbeCLEARSYVerified email at clearsy.com
