default search action
Pascal Fontaine
Person information
- affiliation: University of Liège, Belgium
- affiliation: INRIA, France
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
2020 – today
- 2024
- [c46]Bernard Boigelot
, Pascal Fontaine
Non-emptiness Test for Automata over Words Indexed by the Reals and Rationals. CIAA 2024: 94-108 - [i11]Geoff Sutcliffe, Alexander Steen, Pascal Fontaine:
The New TPTP Format for Interpretations. CoRR abs/2406.06108 (2024) - 2023
- [c45]Bernard Boigelot
Decidability of Difference Logic over the Reals with Uninterpreted Unary Predicates. CADE 2023: 542-559 - [c44]Alexander Steen
Representation, Verification, and Visualization of Tarskian Interpretations for Typed First-order Logic. LPAR 2023: 369-385 - [c43]Bernard Boigelot
Universal First-Order Quantification over Automata. CIAA 2023: 91-102 - [e9]Daniele Nantes-Sobrinho, Pascal Fontaine:
Proceedings 17th International Workshop on Logical and Semantic Frameworks with Applications, LSFA 2022, Belo Horizonte, Brazil (hybrid), 23-24 September 2022. EPTCS 376, 2023 [contents] - [i10]Bernard Boigelot, Pascal Fontaine, Baptiste Vergain:
Decidability of Difference Logic over the Reals with Uninterpreted Unary Predicates. CoRR abs/2305.15059 (2023) - [i9]Bernard Boigelot, Pascal Fontaine, Baptiste Vergain:
First-Order Quantification over Automata. CoRR abs/2306.04210 (2023) - [i8]Maria Paola Bonacina, Pascal Fontaine, Cláudia Nalon, Claudia Schon, Martin Desharnais:
The Next Generation of Deduction Systems: From Composition to Compositionality (Dagstuhl Seminar 23471). Dagstuhl Reports 13(11): 130-150 (2023) - 2022
- [j10]Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark W. Barrett
Polite Combination of Algebraic Datatypes. J. Autom. Reason. 66(3): 331-355 (2022) - [c42]Bernard Boigelot, Pascal Fontaine, Baptiste Vergain:
Decidability of difference logics with unary predicates. SC-Square@FLoC 2022: 25-36 - 2021
- [j9]Pascal Fontaine:
Preface: Special Issue of Selected Extended Papers of CADE 2019. J. Autom. Reason. 65(7): 891-892 (2021) - [c41]Mikolás Janota, Haniel Barbosa, Pascal Fontaine, Andrew Reynolds:
Fair and Adventurous Enumeration of Quantifier Instantiations. FMCAD 2021: 256-260 - [c40]Pascal Fontaine
Quantifier Simplification by Unification in SMT. FroCoS 2021: 232-249 - [c39]Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark W. Barrett:
Politeness for the Theory of Algebraic Datatypes (Extended Abstract). IJCAI 2021: 4829-4833 - [c38]Bernard Boigelot, Pascal Fontaine, Baptiste Vergain:
Deciding Satisfiability for Fragments with Unary Predicates and Difference Arithmetic (short paper). SC-Square@SIAM AG 2021: 18-26 - [c37]Hans-Jörg Schurr, Mathias Fleury
Alethe: Towards a Generic SMT Proof Format (extended abstract). PxTP 2021: 49-54 - [i7]Mikolás Janota, Haniel Barbosa, Pascal Fontaine, Andrew Reynolds:
Fair and Adventurous Enumeration of Quantifier Instantiations. CoRR abs/2105.13700 (2021) - 2020
- [j8]Paula Daniela Chocron
Politeness and Combination Methods for Theories with Bridging Functions. J. Autom. Reason. 64(1): 97-134 (2020) - [j7]Haniel Barbosa
Scalable Fine-Grained Proofs for Formula Processing. J. Autom. Reason. 64(3): 485-510 (2020) - [c36]Ying Sheng
Politeness for the Theory of Algebraic Datatypes. IJCAR (1) 2020: 238-255 - [c35]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: 3-14 - [e8]Pascal Fontaine, Konstantin Korovin, Ilias S. Kotsireas, Philipp Rümmer, Sophie Tourret:
Joint Proceedings of the 7th Workshop on Practical Aspects of Automated Reasoning (PAAR) and the 5th Satisfiability Checking and Symbolic Computation Workshop (SC-Square) Workshop, 2020 co-located with the 10th International Joint Conference on Automated Reasoning (IJCAR 2020), Paris, France, June-July, 2020 (Virtual). CEUR Workshop Proceedings 2752, CEUR-WS.org 2020 [contents] - [i6]Ying Sheng
Politeness for the Theory of Algebraic Datatypes. CoRR abs/2004.04854 (2020)
2010 – 2019
- 2019
- [c34]Maria Paola Bonacina, Pascal Fontaine, Christophe Ringeissen, Cesare Tinelli
Theory Combination: Beyond Equality Sharing. Description Logic, Theory Combination, and All That 2019: 57-89 - [e7]Pascal Fontaine:
Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings. Lecture Notes in Computer Science 11716, Springer 2019, ISBN 978-3-030-29435-9 [contents] - 2018
- [b1]Pascal Fontaine:
Satisfiability Modulo Theories: state-of-the-art, contributions, project. (Satisfaisabilité Modulo Théories: état de l'art, contributions, projet). University of Lorraine, Nancy, France, 2018 - [j6]Pascal Fontaine, Cezary Kaliszyk, Stephan Schulz, Josef Urban:
Foreword to the Special Issue on Automated Reasoning. AI Commun. 31(3): 235-236 (2018) - [c33]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: 110 - [c32]Andrew Reynolds, Haniel Barbosa
Revisiting Enumerative Instantiation. TACAS (2) 2018: 112-131 - 2017
- [j5]Andreas Fellner
NP-completeness of small conflict set generation for congruence closure. Formal Methods Syst. Des. 51(3): 533-544 (2017) - [c31]Erika Ábrahám
SC-square: when Satisfiability Checking and Symbolic Computation join forces. ARCADE@CADE 2017: 6-10 - [c30]Jasmin Christian Blanchette, Pascal Fontaine, Stephan Schulz, Uwe Waldmann:
Towards Strong Higher-Order Automation for Fast Interactive Verification. ARCADE@CADE 2017: 16-23 - [c29]Haniel Barbosa
Scalable Fine-Grained Proofs for Formula Processing. CADE 2017: 398-412 - [c28]Pascal Fontaine
Subtropical Satisfiability. FroCoS 2017: 189-206 - [c27]Haniel Barbosa
Congruence Closure with Free Variables. TACAS (2) 2017: 214-230 - [c26]Haniel Barbosa
Language and Proofs for Higher-Order SMT (Work in Progress). PxTP 2017: 15-22 - [e6]Erika Ábrahám, James H. Davenport, Pascal Fontaine:
Proceedings of the 1st Workshop on Satisfiability Checking and Symbolic Computation co-located with 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC 2016), Timisoara, Romania, September 24, 2016. CEUR Workshop Proceedings 1804, CEUR-WS.org 2017 [contents] - [i5]Pascal Fontaine, Mizuhito Ogawa, Thomas Sturm, Xuan-Tung Vu:
Subtropical Satisfiability. CoRR abs/1706.09236 (2017) - 2016
- [j4]Erika Ábrahám
Satisfiability checking and symbolic computation. ACM Commun. Comput. Algebra 50(4): 145-147 (2016) - [c25]Erika Ábrahám
SC2: Satisfiability Checking Meets Symbolic Computation - (Project Paper). CICM 2016: 28-43 - [e5]Pascal Fontaine, Stephan Schulz, Josef Urban:
Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning co-located with International Joint Conference on Automated Reasoning (IJCAR 2016), Coimbra, Portugal, July 2nd, 2016. CEUR Workshop Proceedings 1635, CEUR-WS.org 2016 [contents] - [i4]Erika Ábrahám
Satisfiability Checking and Symbolic Computation. CoRR abs/1607.06945 (2016) - [i3]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 abs/1607.08028 (2016) - 2015
- [j3]Pascal Fontaine, Thomas Sturm
Foreword to the Special Focus on Constraints and Combinations. Math. Comput. Sci. 9(3): 265 (2015) - [c24]Carlos Areces
Modal Satisfiability via SMT Solving. Software, Services, and Systems 2015: 30-45 - [c23]Paula Daniela Chocron
A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited. CADE 2015: 419-433 - [c22]Maximilian Jaroschek, Pablo Federico Dobal, Pascal Fontaine:
Adapting Real Quantifier Elimination Methods for Conflict Set Computation. FroCos 2015: 151-166 - [c21]Paula Daniela Chocron
A Rewriting Approach to the Combination of Data Structures with Bridging Theories. FroCos 2015: 275-290 - [i2]Maximilian Jaroschek, Pablo Federico Dobal, Pascal Fontaine:
Adapting Real Quantifier Elimination Methods for Conflict Set Computation. CoRR abs/1511.01123 (2015) - [i1]Erika Ábrahám, Pascal Fontaine, Thomas Sturm, Dongming Wang:
Symbolic Computation and Satisfiability Checking (Dagstuhl Seminar 15471). Dagstuhl Reports 5(11): 71-89 (2015) - 2014
- [j2]David Déharbe
Integrating SMT solvers in Rodin. Sci. Comput. Program. 94: 130-143 (2014) - [c20]Paula Daniela Chocron
A Gentle Non-disjoint Combination of Satisfiability Procedures. IJCAR 2014: 122-136 - 2013
- [c19]David Déharbe, Pascal Fontaine, Daniel Le Berre, Bertrand Mazure:
Computing prime implicants. FMCAD 2013: 46-52 - [e4]Pascal Fontaine, Amit Goel:
10th International Workshop on Satisfiability Modulo Theories, SMT 2012, Manchester, UK, June 30 - July 1, 2012. EPiC Series in Computing 20, EasyChair 2013 [contents] - [e3]Pascal Fontaine, Renate A. Schmidt, Stephan Schulz:
Third Workshop on Practical Aspects of Automated Reasoning, PAAR-2012, Manchester, UK, June 30 - July 1, 2012. EPiC Series in Computing 21, EasyChair 2013 [contents] - [e2]Pascal Fontaine, Christophe Ringeissen, Renate A. Schmidt:
Frontiers of Combining Systems - 9th International Symposium, FroCoS 2013, Nancy, France, September 18-20, 2013. Proceedings. Lecture Notes in Computer Science 8152, Springer 2013, ISBN 978-3-642-40884-7 [contents] - 2012
- [j1]Diego Caminha Barbosa De Oliveira, David Déharbe, Pascal Fontaine:
Combining decision procedures by (model-)equality propagation. Sci. Comput. Program. 77(4): 518-532 (2012) - [c18]David Déharbe, Pascal Fontaine, Yoann Guyot, Laurent Voisin:
SMT Solvers for Rodin. ABZ 2012: 194-207 - [c17]Pascal Fontaine, Stephan Merz, Christoph Weidenbach:
Combination of Disjoint Theories: Beyond Decidability. IJCAR 2012: 256-270 - 2011
- [c16]David Déharbe, Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo:
Exploiting Symmetry in SMT Problems. CADE 2011: 222-236 - [c15]Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo:
Compression of Propositional Resolution Proofs via Partial Regularization. CADE 2011: 237-251 - [c14]Carlos Areces
Combining Theories: The Ackerman and Guarded Fragments. FroCoS 2011: 40-54 - [c13]Frédéric Besson, Pascal Fontaine, Laurent Théry:
A Flexible Proof Format for SMT: a Proposal. PxTP 2011: 15-26 - [c12]David Déharbe, Pascal Fontaine, Bruno Woltzenlogel Paleo:
Quantifier Inference Rules for SMT proofs. PxTP 2011: 33-39 - [e1]Pascal Fontaine, Aaron Stump:
PxTP 2011: First International Workshop on Proof eXchange for Theorem Proving, Wrocław, Poland, August 1, 2011. 2011 [contents] - 2010
- [c11]Thomas Bouton, Diego Caminha, David Déharbe, Pascal Fontaine:
GridTPT: a distributed platform for Theorem Prover Testing. PAAR@IJCAR 2010: 33-39
2000 – 2009
- 2009
- [c10]Thomas Bouton, Diego Caminha Barbosa De Oliveira, David Déharbe, Pascal Fontaine:
veriT: An Open, Trustable and Efficient SMT-Solver. CADE 2009: 151-156 - [c9]Pascal Fontaine:
Combinations of Theories for Decidable Fragments of First-Order Logic. FroCoS 2009: 263-278 - 2008
- [c8]Diego Caminha Barbosa De Oliveira, David Déharbe
Combining Decision Procedures by (Model-)Equality Propagation. SBMF 2008: 113-128 - 2007
- [c7]Pascal Fontaine:
Combinations of Theories and the Bernays-Schönfinkel-Ramsey Class. VERIFY 2007 - 2006
- [c6]David Déharbe, Pascal Fontaine, Silvio Ranise, Christophe Ringeissen:
Decision Procedures for the Formal Analysis of Software. ICTAC 2006: 366-370 - [c5]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: 167-181 - 2004
- [c4]Pascal Fontaine, Silvio Ranise, Calogero G. Zarba:
Combining Lists with Non-stably Infinite Theories. LPAR 2004: 51-66 - [c3]Pascal Fontaine, E. Pascal Gribomont:
Combining Non-stably Infinite, Non-first Order Theories. D/PDPAR@IJCAR 2004: 37-51 - 2003
- [c2]Pascal Fontaine, E. Pascal Gribomont:
Decidability of Invariant Validation for Paramaterized Systems. TACAS 2003: 97-112 - 2002
- [c1]Pascal Fontaine, E. Pascal Gribomont:
Using BDDs with Combinations of Theories. LPAR 2002: 190-201
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-10-13 17:57 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: