Using BDDs with Combinations of Theories. - Pascal Fontaine; E. Pascal Gribomont (LPAR, 2002)

Decidability of Invariant Validation for Paramaterized Systems. - Pascal Fontaine; E. Pascal Gribomont (TACAS, 2003)

Combining Lists with Non-stably Infinite Theories. - Pascal Fontaine; Silvio Ranise; Calogero G. Zarba (LPAR, 2004)

Combining Non-stably Infinite, Non-first Order Theories. - Pascal Fontaine; E. Pascal Gribomont (D/PDPAR@IJCAR, 2004)

Decision Procedures for the Formal Analysis of Software. - David Déharbe; Pascal Fontaine; Silvio Ranise; Christophe Ringeissen (ICTAC, 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 (TACAS, 2006)

Combinations of Theories and the Bernays-Schönfinkel-Ramsey Class. - Pascal Fontaine (VERIFY, 2007)

veriT: An Open, Trustable and Efficient SMT-Solver. - Thomas Bouton; Diego Caminha Barbosa De Oliveira; David Déharbe; Pascal Fontaine (CADE, 2009)

Combinations of Theories for Decidable Fragments of First-Order Logic. - Pascal Fontaine (FroCoS, 2009)

GridTPT: a distributed platform for Theorem Prover Testing. - Thomas Bouton; Diego Caminha; David Déharbe; Pascal Fontaine (PAAR@IJCAR, 2010)

Exploiting Symmetry in SMT Problems. - David Déharbe; Pascal Fontaine; Stephan Merz; Bruno Woltzenlogel Paleo (CADE, 2011)

Compression of Propositional Resolution Proofs via Partial Regularization. - Pascal Fontaine; Stephan Merz; Bruno Woltzenlogel Paleo (CADE, 2011)

Combining Theories: The Ackerman and Guarded Fragments. - Carlos Areces; Pascal Fontaine (FroCoS, 2011)

A Flexible Proof Format for SMT: a Proposal. - Frédéric Besson; Pascal Fontaine; Laurent Théry (PxTP, 2011)

Quantifier Inference Rules for SMT proofs. - David Déharbe; Pascal Fontaine; Bruno Woltzenlogel Paleo (PxTP, 2011)

SMT Solvers for Rodin. - David Déharbe; Pascal Fontaine; Yoann Guyot; Laurent Voisin (ABZ, 2012)

Combination of Disjoint Theories: Beyond Decidability. - Pascal Fontaine; Stephan Merz; Christoph Weidenbach (IJCAR, 2012)

Combining decision procedures by (model-)equality propagation. - Diego Caminha Barbosa De Oliveira; David Déharbe; Pascal Fontaine (Sci. Comput. Program., 2012)

Computing prime implicants. - David Déharbe; Pascal Fontaine; Daniel Le Berre; Bertrand Mazure (FMCAD, 2013)

A Gentle Non-disjoint Combination of Satisfiability Procedures. - Paula Daniela Chocron; Pascal Fontaine; Christophe Ringeissen (IJCAR, 2014)

Integrating SMT solvers in Rodin. - David Déharbe; Pascal Fontaine; Yoann Guyot; Laurent Voisin (Sci. Comput. Program., 2014)

Modal Satisfiability via SMT Solving. - Carlos Areces; Pascal Fontaine; Stephan Merz (Software, Services, and Systems, 2015)

A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited. - Paula Daniela Chocron; Pascal Fontaine; Christophe Ringeissen (CADE, 2015)

A Rewriting Approach to the Combination of Data Structures with Bridging Theories. - Paula Daniela Chocron; Pascal Fontaine; Christophe Ringeissen (FroCos, 2015)

Adapting Real Quantifier Elimination Methods for Conflict Set Computation. - Maximilian Jaroschek; Pablo Federico Dobal; Pascal Fontaine (FroCos, 2015)

Symbolic Computation and Satisfiability Checking (Dagstuhl Seminar 15471). - Erika Ábrahám; Pascal Fontaine; Thomas Sturm 001; Dongming Wang 001 (Dagstuhl Reports, 2015)

Foreword to the Special Focus on Constraints and Combinations. - Pascal Fontaine; Thomas Sturm 001; Uwe Waldmann (Math. Comput. Sci., 2015)

SC2: Satisfiability Checking Meets Symbolic Computation - (Project Paper). - Erika Ábrahám; John Abbott; Bernd Becker 001; Anna Maria Bigatti; Martin Brain; Bruno Buchberger; Alessandro Cimatti; James H. Davenport; Matthew England 001; Pascal Fontaine; Stephen Forrest; Alberto Griggio; et al. (CICM, 2016)

Satisfiability checking and symbolic computation. - Erika Ábrahám; John Abbott; Bernd Becker 001; Anna Maria Bigatti; Martin Brain; Bruno Buchberger; Alessandro Cimatti; James H. Davenport; Matthew England 001; Pascal Fontaine; Stephen Forrest; Alberto Griggio; et al. (ACM Commun. Comput. Algebra, 2016)

Satisfiability Checking meets Symbolic Computation (Project Paper). - Erika Ábrahám; John Abbott; Bernd Becker 001; Anna Maria Bigatti; Martin Brain; Bruno Buchberger; Alessandro Cimatti; James H. Davenport; Matthew England 001; Pascal Fontaine; Stephen Forrest; Alberto Griggio; et al. (CoRR, 2016)

SC-square: when Satisfiability Checking and Symbolic Computation join forces. - Erika Ábrahám; John Abbott; Bernd Becker 001; Anna Maria Bigatti; Martin Brain; Alessandro Cimatti; James H. Davenport; Matthew England 001; Pascal Fontaine; Stephen Forrest; Vijay Ganesh 001; Alberto Griggio; et al. (ARCADE@CADE, 2017)

Scalable Fine-Grained Proofs for Formula Processing. - Haniel Barbosa; Jasmin Christian Blanchette; Pascal Fontaine (CADE, 2017)

Towards Strong Higher-Order Automation for Fast Interactive Verification. - Jasmin Christian Blanchette; Pascal Fontaine; Stephan Schulz 001; Uwe Waldmann (ARCADE@CADE, 2017)

Subtropical Satisfiability. - Pascal Fontaine; Mizuhito Ogawa; Thomas Sturm 001; Xuan-Tung Vu (FroCoS, 2017)

Congruence Closure with Free Variables. - Haniel Barbosa; Pascal Fontaine; Andrew Reynolds 001 (TACAS (2), 2017)

Language and Proofs for Higher-Order SMT (Work in Progress). - Haniel Barbosa; Jasmin Christian Blanchette; Simon Cruanes; Daniel El Ouraoui; Pascal Fontaine (PxTP, 2017)

NP-completeness of small conflict set generation for congruence closure. - Andreas Fellner; Pascal Fontaine; Bruno Woltzenlogel Paleo (Formal Methods Syst. Des., 2017)

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

Wrapping Computer Algebra is Surprisingly Successful for Non-Linear SMT. - Pascal Fontaine; Mizuhito Ogawa; Thomas Sturm 001; To Van Khanh; Xuan-Tung Vu (SC-Square@FLOC, 2018)

Revisiting Enumerative Instantiation. - Andrew Reynolds 001; Haniel Barbosa; Pascal Fontaine (TACAS (2), 2018)

Foreword to the Special Issue on Automated Reasoning. - Pascal Fontaine; Cezary Kaliszyk; Stephan Schulz 001; Josef Urban (AI Commun., 2018)

Theory Combination: Beyond Equality Sharing. - Maria Paola Bonacina; Pascal Fontaine; Christophe Ringeissen; Cesare Tinelli (Description Logic, Theory Combination, and All That, 2019)

Politeness for the Theory of Algebraic Datatypes. - Ying Sheng 007; Yoni Zohar; Christophe Ringeissen; Jane Lange; Pascal Fontaine; Clark W. Barrett (IJCAR (1), 2020)

Lifting Congruence Closure with Free Variables to λ-free Higher-order Logic via SAT Encoding. - Sophie Tourret; Pascal Fontaine; Daniel El Ouraoui; Haniel Barbosa (SMT, 2020)

Scalable Fine-Grained Proofs for Formula Processing. - Haniel Barbosa; Jasmin Christian Blanchette; Mathias Fleury; Pascal Fontaine (J. Autom. Reason., 2020)

Politeness and Combination Methods for Theories with Bridging Functions. - Paula Daniela Chocron; Pascal Fontaine; Christophe Ringeissen (J. Autom. Reason., 2020)

Fair and Adventurous Enumeration of Quantifier Instantiations. - Mikolás Janota; Haniel Barbosa; Pascal Fontaine; Andrew Reynolds 001 (FMCAD, 2021)

Quantifier Simplification by Unification in SMT. - Pascal Fontaine; Hans-Jörg Schurr (FroCoS, 2021)

Politeness for the Theory of Algebraic Datatypes (Extended Abstract). - Ying Sheng 007; Yoni Zohar; Christophe Ringeissen; Jane Lange; Pascal Fontaine; Clark W. Barrett (IJCAI, 2021)

Deciding Satisfiability for Fragments with Unary Predicates and Difference Arithmetic (short paper). - Bernard Boigelot; Pascal Fontaine; Baptiste Vergain (SC-Square@SIAM AG, 2021)

Alethe: Towards a Generic SMT Proof Format (extended abstract). - Hans-Jörg Schurr; Mathias Fleury; Haniel Barbosa; Pascal Fontaine (PxTP, 2021)

Preface: Special Issue of Selected Extended Papers of CADE 2019. - Pascal Fontaine (J. Autom. Reason., 2021)

Decidability of difference logics with unary predicates. - Bernard Boigelot; Pascal Fontaine; Baptiste Vergain (SC-Square@FLoC, 2022)

Polite Combination of Algebraic Datatypes. - Ying Sheng 007; Yoni Zohar; Christophe Ringeissen; Jane Lange; Pascal Fontaine; Clark W. Barrett (J. Autom. Reason., 2022)

Decidability of Difference Logic over the Reals with Uninterpreted Unary Predicates. - Bernard Boigelot; Pascal Fontaine; Baptiste Vergain (CADE, 2023)

Representation, Verification, and Visualization of Tarskian Interpretations for Typed First-order Logic. - Alexander Steen; Geoff Sutcliffe; Pascal Fontaine; Jack McKeown (LPAR, 2023)

Universal First-Order Quantification over Automata. - Bernard Boigelot; Pascal Fontaine; Baptiste Vergain (CIAA, 2023)

First-Order Quantification over Automata. - Bernard Boigelot; Pascal Fontaine; Baptiste Vergain (CoRR, 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)

Non-emptiness Test for Automata over Words Indexed by the Reals and Rationals. - Bernard Boigelot; Pascal Fontaine; Baptiste Vergain (CIAA, 2024)

The New TPTP Format for Interpretations. - Geoff Sutcliffe; Alexander Steen; Pascal Fontaine (CoRR, 2024)

SMT-LIB release 2023 (incremental benchmarks). - Mathias Preiner; Hans-Jörg Schurr; Clark W. Barrett; Pascal Fontaine; Aina Niemetz; Cesare Tinelli (Zenodo, 2024)

SMT-LIB release 2023 (non-incremental benchmarks). - Mathias Preiner; Hans-Jörg Schurr; Clark W. Barrett; Pascal Fontaine; Aina Niemetz; Cesare Tinelli (Zenodo, 2024)

SMT-LIB release 2024 (non-incremental benchmarks). - Mathias Preiner; Hans-Jörg Schurr; Clark W. Barrett; Pascal Fontaine; Aina Niemetz; Cesare Tinelli (Zenodo, 2024)

SMT-LIB release 2024 (incremental benchmarks). - Mathias Preiner; Hans-Jörg Schurr; Clark W. Barrett; Pascal Fontaine; Aina Niemetz; Cesare Tinelli (Zenodo, 2024)

SMT-LIB release 2024 (incremental benchmarks). - Mathias Preiner; Hans-Jörg Schurr; Clark W. Barrett; Pascal Fontaine; Aina Niemetz; Cesare Tinelli (Zenodo, 2024)