Pascal Fontaine

According to our database, Pascal Fontaine authored at least 61 papers between 2002 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of four.

2024

The New TPTP Format for Interpretations.

Geoff Sutcliffe, Alexander Steen, Pascal Fontaine

CoRR, 2024

Non-emptiness Test for Automata over Words Indexed by the Reals and Rationals.

Bernard Boigelot, Pascal Fontaine, Baptiste Vergain

Proceedings of the Implementation and Application of Automata, 2024

2023

The Next Generation of Deduction Systems: From Composition to Compositionality (Dagstuhl Seminar 23471).

Maria Paola Bonacina, Pascal Fontaine, Cláudia Nalon, Claudia Schon, Martin Desharnais

Dagstuhl Reports, 2023

First-Order Quantification over Automata.

Bernard Boigelot, Pascal Fontaine, Baptiste Vergain

CoRR, 2023

Universal First-Order Quantification over Automata.

Bernard Boigelot, Pascal Fontaine, Baptiste Vergain

Proceedings of the Implementation and Application of Automata, 2023

Representation, Verification, and Visualization of Tarskian Interpretations for Typed First-order Logic.

Alexander Steen, Geoff Sutcliffe, Pascal Fontaine, Jack McKeown

Proceedings of the LPAR 2023: Proceedings of 24th International Conference on Logic for Programming, 2023

Decidability of Difference Logic over the Reals with Uninterpreted Unary Predicates.

Bernard Boigelot, Pascal Fontaine, Baptiste Vergain

Proceedings of the Automated Deduction - CADE 29, 2023

2022

Polite Combination of Algebraic Datatypes.

Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark W. Barrett

J. Autom. Reason., 2022

Decidability of difference logics with unary predicates.

Bernard Boigelot, Pascal Fontaine, Baptiste Vergain

Proceedings of the 7th SC-Square Workshop co-located with the Federated Logic Conference, 2022

2021

Preface: Special Issue of Selected Extended Papers of CADE 2019.

Pascal Fontaine

J. Autom. Reason., 2021

Alethe: Towards a Generic SMT Proof Format (extended abstract).

Hans-Jörg Schurr, Mathias Fleury, Haniel Barbosa, Pascal Fontaine

Proceedings of the Proceedings Seventh Workshop on Proof eXchange for Theorem Proving, 2021

Deciding Satisfiability for Fragments with Unary Predicates and Difference Arithmetic (short paper).

Bernard Boigelot, Pascal Fontaine, Baptiste Vergain

Proceedings of the 6th SC-Square Workshop co-located with the SIAM Conference on Applied Algebraic Geometry, 2021

Politeness for the Theory of Algebraic Datatypes (Extended Abstract).

Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark W. Barrett

Proceedings of the Thirtieth International Joint Conference on Artificial Intelligence, 2021

Quantifier Simplification by Unification in SMT.

Pascal Fontaine, Hans-Jörg Schurr

Proceedings of the Frontiers of Combining Systems - 13th International Symposium, 2021

Fair and Adventurous Enumeration of Quantifier Instantiations.

Mikolás Janota, Haniel Barbosa, Pascal Fontaine, Andrew Reynolds

Proceedings of the Formal Methods in Computer Aided Design, 2021

2020

Politeness and Combination Methods for Theories with Bridging Functions.

Paula Daniela Chocron, Pascal Fontaine, Christophe Ringeissen

J. Autom. Reason., 2020

Scalable Fine-Grained Proofs for Formula Processing.

Haniel Barbosa, Jasmin Christian Blanchette, Mathias Fleury, Pascal Fontaine

J. Autom. Reason., 2020

Lifting Congruence Closure with Free Variables to λ-free Higher-order Logic via SAT Encoding.

Sophie Tourret, Pascal Fontaine, Daniel El Ouraoui, Haniel Barbosa

Proceedings of the 18th International Workshop on Satisfiability Modulo Theories co-located with the 10th International Joint Conference on Automated Reasoning (IJCAR 2020), 2020

Politeness for the Theory of Algebraic Datatypes.

Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark W. Barrett

Proceedings of the Automated Reasoning - 10th International Joint Conference, 2020

2019

Theory Combination: Beyond Equality Sharing.

Maria Paola Bonacina, Pascal Fontaine, Christophe Ringeissen, Cesare Tinelli

Proceedings of the Description Logic, Theory Combination, and All That, 2019

2018

Foreword to the Special Issue on Automated Reasoning.

Pascal Fontaine, Cezary Kaliszyk, Stephan Schulz, Josef Urban

AI Commun., 2018

Revisiting Enumerative Instantiation.

Andrew Reynolds, Haniel Barbosa, Pascal Fontaine

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2018

Wrapping Computer Algebra is Surprisingly Successful for Non-Linear SMT.

Pascal Fontaine, Mizuhito Ogawa, Thomas Sturm, To Van Khanh, Xuan-Tung Vu

Proceedings of the 3rd Workshop on Satisfiability Checking and Symbolic Computation co-located with Federated Logic Conference, 2018

Satisfiability Modulo Theories: state-of-the-art, contributions, project. (Satisfaisabilité Modulo Théories: état de l'art, contributions, projet).

Pascal Fontaine

, 2018

2017

NP-completeness of small conflict set generation for congruence closure.

Andreas Fellner, Pascal Fontaine, Bruno Woltzenlogel Paleo

Formal Methods Syst. Des., 2017

Language and Proofs for Higher-Order SMT (Work in Progress).

Haniel Barbosa, Jasmin Christian Blanchette, Simon Cruanes, Daniel El Ouraoui, Pascal Fontaine

Proceedings of the Fifth Workshop on Proof eXchange for Theorem Proving, 2017

Congruence Closure with Free Variables.

Haniel Barbosa, Pascal Fontaine, Andrew Reynolds

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2017

Subtropical Satisfiability.

Pascal Fontaine, Mizuhito Ogawa, Thomas Sturm, Xuan-Tung Vu

Proceedings of the Frontiers of Combining Systems - 11th International Symposium, 2017

Towards Strong Higher-Order Automation for Fast Interactive Verification.

Jasmin Christian Blanchette, Pascal Fontaine, Stephan Schulz, Uwe Waldmann

Proceedings of the ARCADE 2017, 2017

Scalable Fine-Grained Proofs for Formula Processing.

Haniel Barbosa, Jasmin Christian Blanchette, Pascal Fontaine

Proceedings of the Automated Deduction - CADE 26, 2017

SC-square: when Satisfiability Checking and Symbolic Computation join forces.

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

Proceedings of the ARCADE 2017, 2017

2016

Satisfiability Checking meets Symbolic Computation (Project Paper).

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

CoRR, 2016

Satisfiability checking and symbolic computation.

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

ACM Commun. Comput. Algebra, 2016

SC²: Satisfiability Checking Meets Symbolic Computation - (Project Paper).

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

Proceedings of the Intelligent Computer Mathematics - 9th International Conference, 2016

2015

Foreword to the Special Focus on Constraints and Combinations.

Pascal Fontaine, Thomas Sturm, Uwe Waldmann

Math. Comput. Sci., 2015

Symbolic Computation and Satisfiability Checking (Dagstuhl Seminar 15471).

Erika Ábrahám, Pascal Fontaine, Thomas Sturm, Dongming Wang

Dagstuhl Reports, 2015

Adapting Real Quantifier Elimination Methods for Conflict Set Computation.

Maximilian Jaroschek, Pablo Federico Dobal, Pascal Fontaine

Proceedings of the Frontiers of Combining Systems - 10th International Symposium, 2015

A Rewriting Approach to the Combination of Data Structures with Bridging Theories.

Paula Daniela Chocron, Pascal Fontaine, Christophe Ringeissen

Proceedings of the Frontiers of Combining Systems - 10th International Symposium, 2015

A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited.

Paula Daniela Chocron, Pascal Fontaine, Christophe Ringeissen

Proceedings of the Automated Deduction - CADE-25, 2015

Modal Satisfiability via SMT Solving.

Carlos Areces, Pascal Fontaine, Stephan Merz

Proceedings of the Software, 2015

2014

Integrating SMT solvers in Rodin.

David Déharbe, Pascal Fontaine, Yoann Guyot, Laurent Voisin

Sci. Comput. Program., 2014

A Gentle Non-disjoint Combination of Satisfiability Procedures.

Paula Daniela Chocron, Pascal Fontaine, Christophe Ringeissen

Proceedings of the Automated Reasoning - 7th International Joint Conference, 2014

2013

Computing prime implicants.

David Déharbe, Pascal Fontaine, Daniel Le Berre, Bertrand Mazure

Proceedings of the Formal Methods in Computer-Aided Design, 2013

2012

Combining decision procedures by (model-)equality propagation.

Diego Caminha Barbosa De Oliveira, David Déharbe, Pascal Fontaine

Sci. Comput. Program., 2012

Combination of Disjoint Theories: Beyond Decidability.

Pascal Fontaine, Stephan Merz, Christoph Weidenbach

Proceedings of the Automated Reasoning - 6th International Joint Conference, 2012

SMT Solvers for Rodin.

David Déharbe, Pascal Fontaine, Yoann Guyot, Laurent Voisin

Proceedings of the Abstract State Machines, Alloy, B, VDM, and Z, 2012

2011

Quantifier Inference Rules for SMT proofs.

David Déharbe, Pascal Fontaine, Bruno Woltzenlogel Paleo

Proceedings of the PxTP 2011: First International Workshop on Proof eXchange for Theorem Proving, 2011

A Flexible Proof Format for SMT: a Proposal.

Frédéric Besson, Pascal Fontaine, Laurent Théry

Proceedings of the PxTP 2011: First International Workshop on Proof eXchange for Theorem Proving, 2011

Combining Theories: The Ackerman and Guarded Fragments.

Carlos Areces, Pascal Fontaine

Proceedings of the Frontiers of Combining Systems, 8th International Symposium, 2011

Compression of Propositional Resolution Proofs via Partial Regularization.

Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo

Proceedings of the Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31, 2011

Exploiting Symmetry in SMT Problems.

David Déharbe, Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo

Proceedings of the Automated Deduction - CADE-23 - 23rd International Conference on Automated Deduction, Wroclaw, Poland, July 31, 2011

2010

GridTPT: a distributed platform for Theorem Prover Testing.

Thomas Bouton, Diego Caminha, David Déharbe, Pascal Fontaine

Proceedings of the 2nd Workshop on Practical Aspects of Automated Reasoning, 2010

2009

Combinations of Theories for Decidable Fragments of First-Order Logic.

Pascal Fontaine

Proceedings of the Frontiers of Combining Systems, 7th International Symposium, 2009

veriT: An Open, Trustable and Efficient SMT-Solver.

Thomas Bouton, Diego Caminha Barbosa De Oliveira, David Déharbe, Pascal Fontaine

Proceedings of the Automated Deduction, 2009

2007

Combinations of Theories and the Bernays-Schönfinkel-Ramsey Class.

Pascal Fontaine

Proceedings of 4th International Verification Workshop in connection with CADE-21, 2007

2006

Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants.

Pascal Fontaine, Jean-Yves Marion, Stephan Merz, Leonor Prensa Nieto, Alwen Fernanto Tiu

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2006

Decision Procedures for the Formal Analysis of Software.

David Déharbe, Pascal Fontaine, Silvio Ranise, Christophe Ringeissen

Proceedings of the Theoretical Aspects of Computing, 2006

2004

Combining Non-stably Infinite, Non-first Order Theories.

Pascal Fontaine, E. Pascal Gribomont

Proceedings of the Selected Papers from the Workshops on Disproving, 2004

Combining Lists with Non-stably Infinite Theories.

Pascal Fontaine, Silvio Ranise, Calogero G. Zarba

Proceedings of the Logic for Programming, 2004

2003

Decidability of Invariant Validation for Paramaterized Systems.

Pascal Fontaine, E. Pascal Gribomont

Proceedings of the Tools and Algorithms for the Construction and Analysis of Systems, 2003

2002

Using BDDs with Combinations of Theories.

Pascal Fontaine, E. Pascal Gribomont

Proceedings of the Logic for Programming, 2002