Pascal Fontaine

80 papers A* 1A 11B 5C 5Journal 23Unranked 26

Year	Rank	Type	Title / Venue / Authors
2026	—	`conf`	Exploring the SMT-LIB Benchmark Library. TACAS (1) Hans-Jörg Schurr, François Bobot, Mathias Preiner, Aina Niemetz, Clark W. Barrett, Pascal Fontaine, Cesare Tinelli
2026	J	`jnl`	On the Theory of Order Over Real Numbers. Math. Comput. Sci. Bernard Boigelot, Pascal Fontaine, Baptiste Vergain
2026	J	`jnl`	Universal First-Order Quantification over Automata. Int. J. Found. Comput. Sci. Bernard Boigelot, Pascal Fontaine, Baptiste Vergain
2024	C	`conf`	Non-emptiness Test for Automata over Words Indexed by the Reals and Rationals. CIAA Bernard Boigelot, Pascal Fontaine, Baptiste Vergain
2024	J	`jnl`	The New TPTP Format for Interpretations. CoRR Geoff Sutcliffe, Alexander Steen, Pascal Fontaine
2023	A	`conf`	Decidability of Difference Logic over the Reals with Uninterpreted Unary Predicates. CADE Bernard Boigelot, Pascal Fontaine, Baptiste Vergain
2023	J	`jnl`	Decidability of Difference Logic over the Reals with Uninterpreted Unary Predicates. CoRR Bernard Boigelot, Pascal Fontaine, Baptiste Vergain
2023	J	`jnl`	First-Order Quantification over Automata. CoRR Bernard Boigelot, Pascal Fontaine, Baptiste Vergain
2023	—	`ed.`	Proceedings 17th International Workshop on Logical and Semantic Frameworks with Applications, LSFA 2022, Belo Horizonte, Brazil (hybrid), 23-24 September 2022. LSFA Daniele Nantes-Sobrinho, Pascal Fontaine
2023	B	`conf`	Representation, Verification, and Visualization of Tarskian Interpretations for Typed First-order Logic. LPAR Alexander Steen, Geoff Sutcliffe, Pascal Fontaine, Jack McKeown
2023	J	`jnl`	The Next Generation of Deduction Systems: From Composition to Compositionality (Dagstuhl Seminar 23471). Dagstuhl Reports Maria Paola Bonacina, Pascal Fontaine, Cláudia Nalon, Claudia Schon, Martin Desharnais
2023	C	`conf`	Universal First-Order Quantification over Automata. CIAA Bernard Boigelot, Pascal Fontaine, Baptiste Vergain
2022	—	`conf`	Decidability of difference logics with unary predicates. SC-Square@FLoC Bernard Boigelot, Pascal Fontaine, Baptiste Vergain
2022	J	`jnl`	Polite Combination of Algebraic Datatypes. J. Autom. Reason. Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark W. Barrett
2021	—	`conf`	Alethe: Towards a Generic SMT Proof Format (extended abstract). PxTP Hans-Jörg Schurr, Mathias Fleury, Haniel Barbosa, Pascal Fontaine
2021	—	`conf`	Deciding Satisfiability for Fragments with Unary Predicates and Difference Arithmetic (short paper). SC-Square@SIAM AG Bernard Boigelot, Pascal Fontaine, Baptiste Vergain
2021	B	`conf`	Fair and Adventurous Enumeration of Quantifier Instantiations. FMCAD Mikolás Janota, Haniel Barbosa, Pascal Fontaine, Andrew Reynolds
2021	J	`jnl`	Fair and Adventurous Enumeration of Quantifier Instantiations. CoRR Mikolás Janota, Haniel Barbosa, Pascal Fontaine, Andrew Reynolds
2021	A*	`conf`	Politeness for the Theory of Algebraic Datatypes (Extended Abstract). IJCAI Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark W. Barrett
2021	J	`jnl`	Preface: Special Issue of Selected Extended Papers of CADE 2019. J. Autom. Reason. Pascal Fontaine
2021	—	`conf`	Quantifier Simplification by Unification in SMT. FroCoS Pascal Fontaine, Hans-Jörg Schurr
2020	—	`ed.`	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). PAAR+SC²@IJCAR Pascal Fontaine, Konstantin Korovin, Ilias S. Kotsireas, Philipp Rümmer, Sophie Tourret
2020	—	`conf`	Lifting Congruence Closure with Free Variables to λ-free Higher-order Logic via SAT Encoding. SMT Sophie Tourret, Pascal Fontaine, Daniel El Ouraoui, Haniel Barbosa
2020	J	`jnl`	Politeness and Combination Methods for Theories with Bridging Functions. J. Autom. Reason. Paula Daniela Chocron, Pascal Fontaine, Christophe Ringeissen
2020	—	`conf`	Politeness for the Theory of Algebraic Datatypes. IJCAR (1) Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark W. Barrett
2020	J	`jnl`	Politeness for the Theory of Algebraic Datatypes. CoRR Ying Sheng, Yoni Zohar, Christophe Ringeissen, Jane Lange, Pascal Fontaine, Clark W. Barrett
2020	J	`jnl`	Scalable Fine-Grained Proofs for Formula Processing. J. Autom. Reason. Haniel Barbosa, Jasmin Christian Blanchette, Mathias Fleury, Pascal Fontaine
2019	A	`ed.`	Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings CADE Pascal Fontaine
2019	—	`conf`	Theory Combination: Beyond Equality Sharing. Description Logic, Theory Combination, and All That Maria Paola Bonacina, Pascal Fontaine, Christophe Ringeissen, Cesare Tinelli
2018	J	`jnl`	Foreword to the Special Issue on Automated Reasoning. AI Commun. Pascal Fontaine, Cezary Kaliszyk, Stephan Schulz, Josef Urban
2018	—	`conf`	Revisiting Enumerative Instantiation. TACAS (2) Andrew Reynolds, Haniel Barbosa, Pascal Fontaine
2018	—	`book`	Satisfiability Modulo Theories: state-of-the-art, contributions, project. (Satisfaisabilité Modulo Théories: état de l'art, contributions, projet). Pascal Fontaine
2018	—	`conf`	Wrapping Computer Algebra is Surprisingly Successful for Non-Linear SMT. SC-Square@FLOC Pascal Fontaine, Mizuhito Ogawa, Thomas Sturm, To Van Khanh, Xuan-Tung Vu
2017	—	`conf`	Congruence Closure with Free Variables. TACAS (2) Haniel Barbosa, Pascal Fontaine, Andrew Reynolds
2017	—	`conf`	Language and Proofs for Higher-Order SMT (Work in Progress). PxTP Haniel Barbosa, Jasmin Christian Blanchette, Simon Cruanes, Daniel El Ouraoui, Pascal Fontaine
2017	J	`jnl`	NP-completeness of small conflict set generation for congruence closure. Formal Methods Syst. Des. Andreas Fellner, Pascal Fontaine, Bruno Woltzenlogel Paleo
2017	—	`ed.`	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. SC²@SYNASC Erika Ábrahám, James H. Davenport, Pascal Fontaine
2017	—	`conf`	SC-square: when Satisfiability Checking and Symbolic Computation join forces. ARCADE@CADE 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
2017	A	`conf`	Scalable Fine-Grained Proofs for Formula Processing. CADE Haniel Barbosa, Jasmin Christian Blanchette, Pascal Fontaine
2017	—	`conf`	Subtropical Satisfiability. FroCoS Pascal Fontaine, Mizuhito Ogawa, Thomas Sturm, Xuan-Tung Vu
2017	J	`jnl`	Subtropical Satisfiability. CoRR Pascal Fontaine, Mizuhito Ogawa, Thomas Sturm, Xuan-Tung Vu
2017	—	`conf`	Towards Strong Higher-Order Automation for Fast Interactive Verification. ARCADE@CADE Jasmin Christian Blanchette, Pascal Fontaine, Stephan Schulz, Uwe Waldmann
2016	—	`ed.`	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. PAAR@IJCAR Pascal Fontaine, Stephan Schulz, Josef Urban
2016	C	`conf`	SC CICM 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
2016	J	`jnl`	Satisfiability Checking and Symbolic Computation. CoRR 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
2016	J	`jnl`	Satisfiability Checking meets Symbolic Computation (Project Paper). CoRR 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
2016	J	`jnl`	Satisfiability checking and symbolic computation. ACM Commun. Comput. Algebra 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
2015	A	`conf`	A Polite Non-Disjoint Combination Method: Theories with Bridging Functions Revisited. CADE Paula Daniela Chocron, Pascal Fontaine, Christophe Ringeissen
2015	—	`conf`	A Rewriting Approach to the Combination of Data Structures with Bridging Theories. FroCos Paula Daniela Chocron, Pascal Fontaine, Christophe Ringeissen
2015	—	`conf`	Adapting Real Quantifier Elimination Methods for Conflict Set Computation. FroCos Maximilian Jaroschek, Pablo Federico Dobal, Pascal Fontaine
2015	J	`jnl`	Adapting Real Quantifier Elimination Methods for Conflict Set Computation. CoRR Maximilian Jaroschek, Pablo Federico Dobal, Pascal Fontaine
2015	J	`jnl`	Foreword to the Special Focus on Constraints and Combinations. Math. Comput. Sci. Pascal Fontaine, Thomas Sturm, Uwe Waldmann
2015	—	`conf`	Modal Satisfiability via SMT Solving. Software, Services, and Systems Carlos Areces, Pascal Fontaine, Stephan Merz
2015	J	`jnl`	Symbolic Computation and Satisfiability Checking (Dagstuhl Seminar 15471). Dagstuhl Reports Erika Ábrahám, Pascal Fontaine, Thomas Sturm, Dongming Wang
2014	A	`conf`	A Gentle Non-disjoint Combination of Satisfiability Procedures. IJCAR Paula Daniela Chocron, Pascal Fontaine, Christophe Ringeissen
2014	J	`jnl`	Integrating SMT solvers in Rodin. Sci. Comput. Program. David Déharbe, Pascal Fontaine, Yoann Guyot, Laurent Voisin
2013	—	`ed.`	10th International Workshop on Satisfiability Modulo Theories, SMT 2012, Manchester, UK, June 30 - July 1, 2012 SMT@IJCAR Pascal Fontaine, Amit Goel
2013	B	`conf`	Computing prime implicants. FMCAD David Déharbe, Pascal Fontaine, Daniel Le Berre, Bertrand Mazure
2013	—	`ed.`	Frontiers of Combining Systems - 9th International Symposium, FroCoS 2013, Nancy, France, September 18-20, 2013. Proceedings FroCoS Pascal Fontaine, Christophe Ringeissen, Renate A. Schmidt
2013	—	`ed.`	Third Workshop on Practical Aspects of Automated Reasoning, PAAR-2012, Manchester, UK, June 30 - July 1, 2012 PAAR@IJCAR Pascal Fontaine, Renate A. Schmidt, Stephan Schulz
2012	A	`conf`	Combination of Disjoint Theories: Beyond Decidability. IJCAR Pascal Fontaine, Stephan Merz, Christoph Weidenbach
2012	J	`jnl`	Combining decision procedures by (model-)equality propagation. Sci. Comput. Program. Diego Caminha Barbosa De Oliveira, David Déharbe, Pascal Fontaine
2012	C	`conf`	SMT Solvers for Rodin. ABZ David Déharbe, Pascal Fontaine, Yoann Guyot, Laurent Voisin
2011	—	`conf`	A Flexible Proof Format for SMT: a Proposal. PxTP Frédéric Besson, Pascal Fontaine, Laurent Théry
2011	—	`conf`	Combining Theories: The Ackerman and Guarded Fragments. FroCoS Carlos Areces, Pascal Fontaine
2011	A	`conf`	Compression of Propositional Resolution Proofs via Partial Regularization. CADE Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo
2011	A	`conf`	Exploiting Symmetry in SMT Problems. CADE David Déharbe, Pascal Fontaine, Stephan Merz, Bruno Woltzenlogel Paleo
2011	—	`ed.`	PxTP 2011: First International Workshop on Proof eXchange for Theorem Proving, Wrocław, Poland, August 1, 2011 PxTP Pascal Fontaine, Aaron Stump
2011	—	`conf`	Quantifier Inference Rules for SMT proofs. PxTP David Déharbe, Pascal Fontaine, Bruno Woltzenlogel Paleo
2010	—	`conf`	GridTPT: a distributed platform for Theorem Prover Testing. PAAR@IJCAR Thomas Bouton, Diego Caminha, David Déharbe, Pascal Fontaine
2009	—	`conf`	Combinations of Theories for Decidable Fragments of First-Order Logic. FroCoS Pascal Fontaine
2009	A	`conf`	veriT: An Open, Trustable and Efficient SMT-Solver. CADE Thomas Bouton, Diego Caminha Barbosa De Oliveira, David Déharbe, Pascal Fontaine
2008	—	`conf`	Combining Decision Procedures by (Model-)Equality Propagation. SBMF Diego Caminha Barbosa De Oliveira, David Déharbe, Pascal Fontaine
2007	—	`conf`	Combinations of Theories and the Bernays-Schönfinkel-Ramsey Class. VERIFY Pascal Fontaine
2006	C	`conf`	Decision Procedures for the Formal Analysis of Software. ICTAC David Déharbe, Pascal Fontaine, Silvio Ranise, Christophe Ringeissen
2006	A	`conf`	Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants. TACAS Pascal Fontaine, Jean-Yves Marion, Stephan Merz, Leonor Prensa Nieto, Alwen Fernanto Tiu
2004	B	`conf`	Combining Lists with Non-stably Infinite Theories. LPAR Pascal Fontaine, Silvio Ranise, Calogero G. Zarba
2004	—	`conf`	Combining Non-stably Infinite, Non-first Order Theories. D/PDPAR@IJCAR Pascal Fontaine, E. Pascal Gribomont
2003	A	`conf`	Decidability of Invariant Validation for Paramaterized Systems. TACAS Pascal Fontaine, E. Pascal Gribomont
2002	B	`conf`	Using BDDs with Combinations of Theories. LPAR Pascal Fontaine, E. Pascal Gribomont