| 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 | 243 | 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 | 121 | 2006 |
| SMT solvers for Rodin D Déharbe, P Fontaine, Y Guyot, L Voisin Abstract State Machines, Alloy, B, VDM, and Z: Third International …, 2012 | 72 | 2012 |
| Revisiting enumerative instantiation A Reynolds, H Barbosa, P Fontaine Tools and Algorithms for the Construction and Analysis of Systems: 24th …, 2018 | 55 | 2018 |
| Exploiting Symmetry in SMT Problems. D Déharbe, P Fontaine, S Merz, BW Paleo CADE 6803, 222-236, 2011 | 53 | 2011 |
| : 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 | 51 | 2016 |
| Congruence closure with free variables H Barbosa, P Fontaine, A Reynolds Tools and Algorithms for the Construction and Analysis of Systems: 23rd …, 2017 | 44 | 2017 |
| Integrating SMT solvers in Rodin D Déharbe, P Fontaine, Y Guyot, L Voisin Science of Computer Programming 94, 130-143, 2014 | 42 | 2014 |
| Computing prime implicants D Déharbe, P Fontaine, D Le Berre, B Mazure 2013 Formal Methods in Computer-Aided Design, 46-52, 2013 | 37 | 2013 |
| Scalable fine-grained proofs for formula processing H Barbosa, JC Blanchette, M Fleury, P Fontaine Journal of Automated Reasoning 64 (3), 485-510, 2020 | 36 | 2020 |
| Combinations of theories for decidable fragments of first-order logic P Fontaine Frontiers of Combining Systems: 7th International Symposium, FroCoS 2009 …, 2009 | 35 | 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 | 34 | 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 | 34 | 2011 |
| Proofs in satisfiability modulo theories C Barrett, L De Moura, P Fontaine All about proofs, Proofs for all 55 (1), 23-44, 2015 | 31 | 2015 |
| 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 | 26 | 2011 |
| Subtropical satisfiability P Fontaine, M Ogawa, T Sturm, XT Vu Frontiers of Combining Systems: 11th International Symposium, FroCoS 2017 …, 2017 | 22 | 2017 |
| 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 Automated Reasoning: 7th International Joint Conference, IJCAR 2014, Held as …, 2014 | 21 | 2014 |
| Decidability of invariant validation for paramaterized systems P Fontaine, EP Gribomont TACAS 3 (2619), 97-112, 2003 | 20 | 2003 |
David DeharbeCLEARSYVerified email at clearsy.com
