Pascal Fontaine

Publication Activity (10 Years)

Years Active: 2002-2023
Publications (10 Years): 43

Top Topics

Quantifier Elimination

Extended Abstract

Computer Algebra

Terminological Reasoning

Top Venues

J. Autom. Reason.

Publications

Bernard Boigelot, Pascal Fontaine, Baptiste Vergain
Decidability of Difference Logic over the Reals with Uninterpreted Unary Predicates. CADE (2023)
Alexander Steen, Geoff Sutcliffe, Pascal Fontaine, Jack McKeown
Representation, Verification, and Visualization of Tarskian Interpretations for Typed First-order Logic. LPAR (2023)
Bernard Boigelot, Pascal Fontaine, Baptiste Vergain
First-Order Quantification over Automata. CoRR (2023)
Bernard Boigelot, Pascal Fontaine, Baptiste Vergain
Universal First-Order Quantification over Automata. CIAA (2023)
Daniele Nantes-Sobrinho, Pascal Fontaine
Proceedings 17th International Workshop on Logical and Semantic Frameworks with Applications. CoRR (2023)
Bernard Boigelot, Pascal Fontaine, Baptiste Vergain
Decidability of Difference Logic over the Reals with Uninterpreted Unary Predicates. CoRR (2023)
Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark W. Barrett
Polite Combination of Algebraic Datatypes. J. Autom. Reason. 66 (3) (2022)
Bernard Boigelot, Pascal Fontaine, Baptiste Vergain
Decidability of difference logics with unary predicates. SC-Square@FLoC (2022)
Pascal Fontaine, Hans-Jörg Schurr
Quantifier Simplification by Unification in SMT. FroCoS (2021)
Mikolás Janota, Haniel Barbosa, Pascal Fontaine, Andrew Reynolds
Fair and Adventurous Enumeration of Quantifier Instantiations. CoRR (2021)
Mikolás Janota, Haniel Barbosa, Pascal Fontaine, Andrew Reynolds
Fair and Adventurous Enumeration of Quantifier Instantiations. FMCAD (2021)
Pascal Fontaine
Preface: Special Issue of Selected Extended Papers of CADE 2019. J. Autom. Reason. 65 (7) (2021)
Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark W. Barrett
Politeness for the Theory of Algebraic Datatypes (Extended Abstract). IJCAI (2021)
Hans-Jörg Schurr, Mathias Fleury, Haniel Barbosa, Pascal Fontaine
Alethe: Towards a Generic SMT Proof Format (extended abstract). PxTP (2021)
Bernard Boigelot, Pascal Fontaine, Baptiste Vergain
Deciding Satisfiability for Fragments with Unary Predicates and Difference Arithmetic (short paper). SC-Square@SIAM AG (2021)
Sophie Tourret, Pascal Fontaine, Daniel El Ouraoui, Haniel Barbosa
Lifting Congruence Closure with Free Variables to λ-free Higher-order Logic via SAT Encoding. SMT (2020)
Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark W. Barrett
Politeness for the Theory of Algebraic Datatypes. IJCAR (1) (2020)
Paula Daniela Chocron, Pascal Fontaine, Christophe Ringeissen
Politeness and Combination Methods for Theories with Bridging Functions. J. Autom. Reason. 64 (1) (2020)
Haniel Barbosa, Jasmin Christian Blanchette, Mathias Fleury, Pascal Fontaine
Scalable Fine-Grained Proofs for Formula Processing. J. Autom. Reason. 64 (3) (2020)
Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark W. Barrett
Politeness for the Theory of Algebraic Datatypes. CoRR (2020)
Maria Paola Bonacina, Pascal Fontaine, Christophe Ringeissen, Cesare Tinelli
Theory Combination: Beyond Equality Sharing. Description Logic, Theory Combination, and All That (2019)
Andrew Reynolds, Haniel Barbosa, Pascal Fontaine
Revisiting Enumerative Instantiation. TACAS (2) (2018)
Pascal Fontaine, Mizuhito Ogawa, Thomas Sturm, To Van Khanh, Xuan-Tung Vu
Wrapping Computer Algebra is Surprisingly Successful for Non-Linear SMT. SC-Square@FLOC (2018)
Pascal Fontaine, Cezary Kaliszyk, Stephan Schulz, Josef Urban
Foreword to the Special Issue on Automated Reasoning. AI Commun. 31 (3) (2018)
Haniel Barbosa, Jasmin Christian Blanchette, Simon Cruanes, Daniel El Ouraoui, Pascal Fontaine
Language and Proofs for Higher-Order SMT (Work in Progress). PxTP (2017)
Erika Ábrahám, John Abbott, Bernd Becker, Anna Maria Bigatti, Martin Brain, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Vijay Ganesh, Alberto Griggio, Daniel Kroening, Werner M. Seiler
SC-square: when Satisfiability Checking and Symbolic Computation join forces. ARCADE@CADE (2017)
Haniel Barbosa, Pascal Fontaine, Andrew Reynolds
Congruence Closure with Free Variables. TACAS (2) (2017)
Jasmin Christian Blanchette, Pascal Fontaine, Stephan Schulz, Uwe Waldmann
Towards Strong Higher-Order Automation for Fast Interactive Verification. ARCADE@CADE (2017)
Pascal Fontaine, Mizuhito Ogawa, Thomas Sturm, Xuan-Tung Vu
Subtropical Satisfiability. FroCoS (2017)
Andreas Fellner, Pascal Fontaine, Bruno Woltzenlogel Paleo
NP-completeness of small conflict set generation for congruence closure. Formal Methods Syst. Des. 51 (3) (2017)
Haniel Barbosa, Jasmin Christian Blanchette, Pascal Fontaine
Scalable Fine-Grained Proofs for Formula Processing. CADE (2017)
Pascal Fontaine, Mizuhito Ogawa, Thomas Sturm, Xuan-Tung Vu
Subtropical Satisfiability. CoRR (2017)
Erika Ábrahám, John Abbott, Bernd Becker, Anna Maria Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner M. Seiler, Thomas Sturm
Satisfiability Checking meets Symbolic Computation (Project Paper). CoRR (2016)
Erika Ábrahám, John Abbott, Bernd Becker, Anna Maria Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner M. Seiler, Thomas Sturm
Satisfiability Checking and Symbolic Computation. CoRR (2016)
Erika Ábrahám, John Abbott, Bernd Becker, Anna Maria Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner M. Seiler, Thomas Sturm
Satisfiability checking and symbolic computation. ACM Commun. Comput. Algebra 50 (4) (2016)
Erika Ábrahám, John Abbott, Bernd Becker, Anna Maria Bigatti, Martin Brain, Bruno Buchberger, Alessandro Cimatti, James H. Davenport, Matthew England, Pascal Fontaine, Stephen Forrest, Alberto Griggio, Daniel Kroening, Werner M. Seiler, Thomas Sturm
: Satisfiability Checking Meets Symbolic Computation - (Project Paper). CICM (2016)
Carlos Areces, Pascal Fontaine, Stephan Merz
Modal Satisfiability via SMT Solving. Software, Services, and Systems (2015)
Erika Ábrahám, Pascal Fontaine, Thomas Sturm, Dongming Wang
Symbolic Computation and Satisfiability Checking (Dagstuhl Seminar 15471). Dagstuhl Reports 5 (11) (2015)
Pascal Fontaine, Thomas Sturm, Uwe Waldmann
Foreword to the Special Focus on Constraints and Combinations. Math. Comput. Sci. 9 (3) (2015)
Paula Daniela Chocron, Pascal Fontaine, Christophe Ringeissen
A Rewriting Approach to the Combination of Data Structures with Bridging Theories. FroCos (2015)
Maximilian Jaroschek, Pablo Federico Dobal, Pascal Fontaine
Adapting Real Quantifier Elimination Methods for Conflict Set Computation. FroCos (2015)
Maximilian Jaroschek, Pablo Federico Dobal, Pascal Fontaine
Adapting Real Quantifier Elimination Methods for Conflict Set Computation. CoRR (2015)
Paula Daniela Chocron, Pascal Fontaine, Christophe Ringeissen
A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited. CADE (2015)
Paula Daniela Chocron, Pascal Fontaine, Christophe Ringeissen
A Gentle Non-disjoint Combination of Satisfiability Procedures. IJCAR (2014)
David Déharbe, Pascal Fontaine, Yoann Guyot, Laurent Voisin
Integrating SMT solvers in Rodin. Sci. Comput. Program. 94 (2014)
David Déharbe, Pascal Fontaine, Daniel Le Berre, Bertrand Mazure
Computing prime implicants. FMCAD (2013)
Pascal Fontaine, Stephan Merz, Christoph Weidenbach
Combination of Disjoint Theories: Beyond Decidability. IJCAR (2012)
Diego Caminha Barbosa De Oliveira, David Déharbe, Pascal Fontaine
Combining decision procedures by (model-)equality propagation. Sci. Comput. Program. 77 (4) (2012)
David Déharbe, Pascal Fontaine, Yoann Guyot, Laurent Voisin
SMT Solvers for Rodin. ABZ (2012)
David Déharbe, Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo
Exploiting Symmetry in SMT Problems. CADE (2011)
Carlos Areces, Pascal Fontaine
Combining Theories: The Ackerman and Guarded Fragments. FroCoS (2011)
David Déharbe, Pascal Fontaine, Bruno Woltzenlogel Paleo
Quantifier Inference Rules for SMT proofs. PxTP (2011)
Frédéric Besson, Pascal Fontaine, Laurent Théry
A Flexible Proof Format for SMT: a Proposal. PxTP (2011)
Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo
Compression of Propositional Resolution Proofs via Partial Regularization. CADE (2011)
Thomas Bouton, Diego Caminha, David Déharbe, Pascal Fontaine
GridTPT: a distributed platform for Theorem Prover Testing. PAAR@IJCAR (2010)
Thomas Bouton, Diego Caminha Barbosa De Oliveira, David Déharbe, Pascal Fontaine
veriT: An Open, Trustable and Efficient SMT-Solver. CADE (2009)
Diego Caminha Barbosa De Oliveira, David Déharbe, Pascal Fontaine
Combining Decision Procedures by (Model-)Equality Propagation. Electron. Notes Theor. Comput. Sci. 240 (2009)
Pascal Fontaine
Combinations of Theories for Decidable Fragments of First-Order Logic. FroCoS (2009)
Pascal Fontaine
Combinations of Theories and the Bernays-Schönfinkel-Ramsey Class. VERIFY (2007)
David Déharbe, Pascal Fontaine, Silvio Ranise, Christophe Ringeissen
Decision Procedures for the Formal Analysis of Software. ICTAC (2006)
Pascal Fontaine, Jean-Yves Marion, Stephan Merz, Leonor Prensa Nieto, Alwen Fernanto Tiu
Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants. TACAS (2006)
Pascal Fontaine, E. Pascal Gribomont
Combining Non-stably Infinite, Non-first Order Theories. Electron. Notes Theor. Comput. Sci. 125 (3) (2005)
Pascal Fontaine, Silvio Ranise, Calogero G. Zarba
Combining Lists with Non-stably Infinite Theories. LPAR (2004)
Pascal Fontaine, E. Pascal Gribomont
Decidability of Invariant Validation for Paramaterized Systems. TACAS (2003)
Pascal Fontaine, E. Pascal Gribomont
Using BDDs with Combinations of Theories. LPAR (2002)