Accéder directement au contenu

Pascal Fontaine

60
Documents

Publications

Polite Combination of Algebraic Datatypes

Ying Sheng , Yoni Zohar , Christophe Ringeissen , Jane Lange , Pascal Fontaine
Journal of Automated Reasoning, 2022, 66 (3), pp.331-355. ⟨10.1007/s10817-022-09625-3⟩
Article dans une revue hal-03853159v1
Image document

Scalable Fine-Grained Proofs for Formula Processing

Haniel Barbosa , Jasmin Blanchette , Mathias Fleury , Pascal Fontaine
Journal of Automated Reasoning, 2020, 64 (3), pp.485-510. ⟨10.1007/s10817-018-09502-y⟩
Article dans une revue hal-02515103v1
Image document

Politeness and Combination Methods for Theories with Bridging Functions

Paula Chocron , Pascal Fontaine , Christophe Ringeissen
Journal of Automated Reasoning, 2020, 64, pp.97-134. ⟨10.1007/s10817-019-09512-4⟩
Article dans une revue hal-01988452v1
Image document

NP-completeness of small conflict set generation for congruence closure

Andreas Fellner , Pascal Fontaine , Bruno Woltzenlogel Paleo
Formal Methods in System Design, 2017, 51 (3), pp.533 - 544. ⟨10.1007/s10703-017-0283-x⟩
Article dans une revue hal-01908684v1

Satisfiability Checking and Symbolic Computation

Thomas Sturm , Erika Abraham , John A. Abbott , Bern W. Becker , Anna Maria Bigatti
ACM Communications in Computer Algebra, 2016, 50 (4), pp.145-147. ⟨10.1145/3055282.3055285⟩
Article dans une revue hal-01648695v1

Interest rates parity and no arbitrage as equivalent equilibrium conditions in the international financial assets and goods markets

Stefano Bosi , Pascal Fontaine , Cuong Le Van
Mathematical Social Sciences, 2016, 82, pp.26-36. ⟨10.1016/j.mathsocsci.2016.04.002⟩
Article dans une revue hal-01302524v1

Integrating SMT solvers in Rodin

David Déharbe , Pascal Fontaine , Laurent Voisin , Yoann Guyot
Science of Computer Programming, 2014, Abstract State Machines, Alloy, B, VDM, and Z — Selected and extended papers from ABZ 2012, 94, pp.14
Article dans une revue hal-01094999v1

Combining decision procedures by (model-)equality propagation

Diego Caminha B. de Oliveira , David Déharbe , Pascal Fontaine
Science of Computer Programming, 2010, 240 (2 July 2009), pp.113-128. ⟨10.1016/j.entcs.2009.05.048⟩
Article dans une revue inria-00543801v1

Combining Decision Procedures by (Model-)Equality Propagation

Diego Caminha B. de Oliveira , David Déharbe , Pascal Fontaine
Electronic Notes in Theoretical Computer Science, 2009, Proceedings of the Eleventh Brazilian Symposium on Formal Methods (SBMF 2008), 240 (2), pp.113-128. ⟨10.1016/j.entcs.2009.05.048⟩
Article dans une revue inria-00430636v1

Politeness for the Theory of Algebraic Datatypes (Extended Abstract)

Ying Sheng , Yoni Zohar , Christophe Ringeissen , Jane Lange , Pascal Fontaine
IJCAI 2021 - International Joint Conference on Artificial Intelligence (Sister Conferences Best Papers), Aug 2021, Montreal, Canada. pp.4829-4833, ⟨10.24963/ijcai.2021/660⟩
Communication dans un congrès hal-03346697v1
Image document

Quantifier Simplification by Unification in SMT

Pascal Fontaine , Hans-Jörg Schurr
FroCos 2021 - 13th International Symposium on Frontiers of Combining Systems, Sep 2021, Birmingham, United Kingdom. pp.232-249, ⟨10.1007/978-3-030-86205-3_13⟩
Communication dans un congrès hal-03341368v1

Politeness for the Theory of Algebraic Datatypes

Ying Sheng , Yoni Zohar , Christophe Ringeissen , Jane Lange , Pascal Fontaine
10th International Joint Conference on Automated Reasoning, IJCAR, Jul 2020, Paris, France. pp.238--255, ⟨10.1007/978-3-030-51074-9_14⟩
Communication dans un congrès hal-02962716v1
Image document

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 - 18th International Workshop on Satisfiability Modulo Theories, Jul 2020, Online COVID-19, France
Communication dans un congrès hal-03049088v1
Image document

Better SMT Proofs for Easier Reconstruction

Haniel Barbosa , Jasmin Christian Blanchette , Mathias Fleury , Pascal Fontaine , Hans-Jörg Schurr
AITP 2019 - 4th Conference on Artificial Intelligence and Theorem Proving, Apr 2019, Obergurgl, Austria
Communication dans un congrès hal-02381819v1
Image document

Machine Learning for Instance Selection in SMT Solving

Jasmin Christian Blanchette , Daniel El Ouraoui , Pascal Fontaine , Cezary Kaliszyk
AITP 2019 - 4th Conference on Artificial Intelligence and Theorem Proving, Apr 2019, Obergurgl, Austria
Communication dans un congrès hal-02381430v1
Image document

Wrapping Computer Algebra is Surprisingly Successful for Non-Linear SMT

Pascal Fontaine , Mizuhito Ogawa , Thomas Sturm , Van Khanh To , Xuan Tung Vu
SC-square 2018 - Third International Workshop on Satisfiability Checking and Symbolic Computation, Jul 2018, Oxford, United Kingdom
Communication dans un congrès hal-01946733v1
Image document

Revisiting Enumerative Instantiation

Andrew Reynolds , Haniel Barbosa , Pascal Fontaine
TACAS 2018 - 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Apr 2018, Thessaloniki, Greece. pp.20
Communication dans un congrès hal-01877055v1
Image document

Subtropical Satisfiability

Pascal Fontaine , Mizuhito Ogawa , Thomas Sturm , Xuan Vu
FroCoS 2017 - 11th International Symposium on Frontiers of Combining Systems, Sep 2017, Brasilia, Brazil. ⟨10.1007/978-3-319-66167-4⟩
Communication dans un congrès hal-01590899v2
Image document

Scalable Fine-Grained Proofs for Formula Processing

Haniel Barbosa , Jasmin Christian Blanchette , Pascal Fontaine
Proc. Conference on Automated Deduction (CADE), 2017, Gotenburg, Sweden. pp.398 - 412, ⟨10.1007/978-3-642-02959-2_10⟩
Communication dans un congrès hal-01590922v1
Image document

Congruence Closure with Free Variables

Haniel Barbosa , Pascal Fontaine , Andrew Reynolds
TACAS 2017 - 23rd International Conference on Tools and Algorithms for Construction and Analysis of Systems, Apr 2017, Uppsala, Sweden. pp.220 - 230, ⟨10.1007/10721959_17⟩
Communication dans un congrès hal-01590918v1

Towards Strong Higher-Order Automation for Fast Interactive Verification

Jasmin Christian Blanchette , Pascal Fontaine , Stephan Schulz , Uwe Waldmann
ARCADE 2017 - 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements, 2017, Göteborg, Sweden. pp.16-7, ⟨10.29007/3ngx⟩
Communication dans un congrès hal-02359588v1
Image document

SC 2 : Satisfiability Checking meets Symbolic Computation (Project Paper)

Eriká H Abrahám , John Abbott , Bernd Becker , Anna M Bigatti , Martin M Brain
Intelligent Computer Mathematics, Jul 2016, Bialystok, Poland
Communication dans un congrès hal-01377655v1
Image document

Adapting Real Quantifier Elimination Methods for Conflict Set Computation

Maximilian Jaroschek , Pablo Federico Dobal , Pascal Fontaine
Frontiers of Combining Systems (FroCoS), 2015, Wroclaw, Poland. pp.151-166, ⟨10.1007/978-3-319-24246-0_10⟩
Communication dans un congrès hal-01240343v1
Image document

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

Paula Chocron , Pascal Fontaine , Christophe Ringeissen
Frontiers of Combining Systems - 10th International Symposium, FroCoS 2015, Sep 2015, Wroclaw, Poland. pp.275--290, ⟨10.1007/978-3-319-24246-0_17⟩
Communication dans un congrès hal-01206187v1
Image document

Congruence Closure with Free Variables (Work in Progress)

Haniel Barbosa , Pascal Fontaine
QUANTIFY 2015 - 2nd International Workshop on Quantification, Aug 2015, Berlin, Germany
Communication dans un congrès hal-01246036v1
Image document

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

Paula Chocron , Pascal Fontaine , Christophe Ringeissen
25th International Conference on Automated Deduction, CADE-25, Christoph Benzmueller, Aug 2015, Berlin, Germany. pp.419-433, ⟨10.1007/978-3-319-21401-6_29⟩
Communication dans un congrès hal-01157898v1

Proofs in satisfiability modulo theories

Clark Barrett , Leonardo de Moura , Pascal Fontaine
APPA (All about Proofs, Proofs for All), Jul 2014, Vienna, Austria
Communication dans un congrès hal-01095009v1

A Gentle Non-Disjoint Combination of Satisfiability Procedures

Paula Chocron , Pascal Fontaine , Christophe Ringeissen
Automated Reasoning - 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, Jul 2014, Vienna, Austria. pp.122-136, ⟨10.1007/978-3-319-08587-6_9⟩
Communication dans un congrès hal-01087162v1

Satisfiability Modulo Non-Disjoint Combinations of Theories Connected via Bridging Functions

Paula Chocron , Pascal Fontaine , Christophe Ringeissen
Workshop on Automated Deduction: Decidability, Complexity, Tractability, ADDCT 2014. Held as Part of the Vienna Summer of Logic, affiliated with IJCAR 2014 and RTA 2014, Silvio Ghilardi, Ulrike Sattler, Viorica Sofronie-Stokkermans, Jul 2014, Vienna, Austria
Communication dans un congrès hal-01087218v1

Computing prime implicants

David Deharbe , Pascal Fontaine , Daniel Le Berre , Bertrand Mazure
13th International Conference on Formal Methods in Computer-Aided Design (FMCAD'13), Oct 2013, Portland, Oregon, United States. pp.46-52, ⟨10.1109/FMCAD.2013.6679390⟩
Communication dans un congrès hal-03300802v1

SyMT: finding symmetries in SMT formulas

Carlos Areces , David Déharbe , Pascal Fontaine , Orbe Ezequiel
11th International Workshop on Satisfiability Modulo Theories - SMT, Jul 2013, Helsinki, Finland
Communication dans un congrès hal-00867816v1

SMT solvers for Rodin

David Déharbe , Pascal Fontaine , Yoann Guyot , Laurent Voisin
ABZ - Third International Conference on Abstract State Machines, Alloy, B, VDM, and Z - 2012, Jun 2012, Pisa, Italy. pp.194-207, ⟨10.1007/978-3-642-30885-7_14⟩
Communication dans un congrès hal-00747269v1

Combination of disjoint theories: beyond decidability

Pascal Fontaine , Stephan Merz , Christoph Weidenbach
IJCAR - 6th International Joint Conference on Automated Reasoning - 2012, Jun 2012, Manchester, United Kingdom. pp.256-270, ⟨10.1007/978-3-642-31365-3_21⟩
Communication dans un congrès hal-00747271v1
Image document

A Flexible Proof Format for SMT: a Proposal

Frédéric Besson , Pascal Fontaine , Laurent Théry
First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011, Aug 2011, Wrocław, Poland
Communication dans un congrès hal-00642544v1

Compression of Propositional Resolution Proofs via Partial Regularization

Pascal Fontaine , Stephan Merz , Bruno Woltzenlogel Paleo
23rd International Conference on Automated Deduction - CADE-23, Jul 2011, Wroclaw, Poland. pp.237-251, ⟨10.1007/978-3-642-22438-6_19⟩
Communication dans un congrès inria-00617846v1

Combining theories: the Ackerman and Guarded Fragments

Carlos Areces , Pascal Fontaine
8th International Symposium Frontiers of Combining Systems - FroCoS 2011, Viorica Sofronie-Stokkermans, Oct 2011, Saarbrücken, Germany. pp.40--54, ⟨10.1007/978-3-642-24364-6_4⟩
Communication dans un congrès hal-00642529v1

Exploiting Symmetry in SMT Problems

David Déharbe , Pascal Fontaine , Stephan Merz , Bruno Woltzenlogel Paleo
International Conference on Automated Deduction (CADE), Jul 2011, Wroclaw, Poland. pp.222-236, ⟨10.1007/978-3-642-22438-6_18⟩
Communication dans un congrès inria-00617843v1
Image document

Quantifier Inference Rules for SMT proofs

David Déharbe , Pascal Fontaine , Bruno Woltzenlogel Paleo
First International Workshop on Proof eXchange for Theorem Proving - PxTP 2011, Aug 2011, Wrocław, Poland
Communication dans un congrès hal-00642535v1

GridTPT: a distributed platform for Theorem Prover Testing

Thomas Bouton , Diego Caminha B. de Oliveira , David Déharbe , Pascal Fontaine
2nd Workshop on Practical Aspects of Automated Reasoning (PAAR), Jul 2010, Edinburgh, United Kingdom
Communication dans un congrès inria-00543805v1
Image document

Exploring and Exploiting Algebraic and Graphical Properties of Resolution

Pascal Fontaine , Stephan Merz , Bruno Woltzenlogel Paleo
8th International Workshop on Satisfiability Modulo Theories - SMT 2010, Jul 2010, Edinburgh, United Kingdom
Communication dans un congrès inria-00544658v1

veriT: an open, trustable and efficient SMT-solver

Thomas Bouton , Diego Caminha B. de Oliveira , David Déharbe , Pascal Fontaine
22nd International Conference on Automated Deduction - CADE 22, Aug 2009, Montreal, Canada. pp.151-156, ⟨10.1007/978-3-642-02959-2_12⟩
Communication dans un congrès inria-00430634v1

Automating model-based software engineering

David Déharbe , Pascal Fontaine , Anamaria Martins Moreira , Stephan Merz , Anderson Santana de Oliveira
Colloque d'Informatique: Brésil/INRIA (COLIBRI), Jul 2009, Bento Gonçalves, Brazil. pp.22-27
Communication dans un congrès inria-00430637v1

Combinations of theories for decidable fragments of first-order logic

Pascal Fontaine
7th International Symposium, FroCoS 2009, Sep 2009, Trento, Italy. pp.263-278, ⟨10.1007/978-3-642-04222-5_16⟩
Communication dans un congrès inria-00430631v1

Combining decision procedures by (model-)equality propagation

Diego Caminha B. de Oliveira , David Déharbe , Pascal Fontaine
Brazilian Symposium on Formal Methods - SBMF 2008, Aug 2008, Salvador, Bahia, Brazil
Communication dans un congrès inria-00337979v1

Practical Proof Reconstruction for First-order Logic and Set-Theoretical Constructions

Clément Hurlin , Amine Chaib , Pascal Fontaine , Stephan Merz , Tjark Weber
The Isabelle Workshop 2007 - Isabelle'07, Jul 2007, Bremen, Germany. pp.2-13
Communication dans un congrès inria-00186638v1

haRVey : satisfaisabilité et théories

Diego Caminha B. de Oliveira , David Déharbe , Pascal Fontaine
Approches Formelles dans l'Assistance au Développement de Logiciels - AFADL'07, Jun 2007, Namur, Belgique. pp.287-288
Communication dans un congrès inria-00186640v1

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

Pascal Fontaine
4th International Verification Workshop - VERIFY'07, Jul 2007, Bremen, Germany. pp.37-54
Communication dans un congrès inria-00186639v1

Decision Procedures for the Formal Analysis of Software

David Déharbe , Pascal Fontaine , Silvio Ranise , Christophe Ringeissen
3rd International Colloquium on Theoretical Aspects of Computing, ICTAC, Nov 2006, Tunis, Tunisia, pp.366--370, ⟨10.1007/11921240_26⟩
Communication dans un congrès inria-00117277v1

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

Pascal Fontaine , Jean-Yves Marion , Stephan Merz , Leonor Prensa Nieto , Alwen Tiu
12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems - TACAS'06, Mar 2006, Vienna/Austria, pp.167-181, ⟨10.1007/11691372_11⟩
Communication dans un congrès inria-00001088v1
Image document

haRVey: combining reasoners

David Déharbe , Pascal Fontaine
Automatic Verification of Critical Systems - AVoCS 2006, Sep 2006, Nancy/France, pp.152-156
Communication dans un congrès inria-00091662v1
Image document

Combining Lists with Non-Stably Infinite Theories

Pascal Fontaine , Silvio Ranise , Calogero G. Zarba
11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'04), Mar 2005, Montevideo/Uruguay, pp.51--66, ⟨10.1007/b106931⟩
Communication dans un congrès inria-00000481v1

Foreword to the Special Focus on Constraints and Combinations

Pascal Fontaine , Thomas Sturm , Uwe Waldmann
Dongming Wang. Springer, 9 (3), 2015, Mathematics in Computer Science, ⟨10.1007/s11786-015-0239-8⟩
Ouvrages hal-01239438v1

Frontiers of Combining Systems

Pascal Fontaine , Christophe Ringeissen , Renate Schmidt
Pascal Fontaine and Christophe Ringeissen and Renate Schmidt. Springer, 8152, pp.359, 2013, Lecture Notes in Artificial Intelligence, 978-3-642-40884-7
Ouvrages hal-00868424v1
Image document

Theory Combination: Beyond Equality Sharing

Maria Paola Bonacina , Pascal Fontaine , Christophe Ringeissen , Cesare Tinelli
Carsten Lutz; Uli Sattler; Cesare Tinelli; Anni-Yasmin Turhan; Frank Wolter. Description Logic, Theory Combination, and All That - Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday, 11560, Springer, pp.57-89, 2019, Theoretical Computer Science and General Issues, 978-3-030-22101-0
Chapitre d'ouvrage hal-02194001v1
Image document

Modal Satisfiability via SMT Solving

Carlos Areces , Pascal Fontaine , Stephan Merz
Software, Services, and Systems. Essays Dedicated to Martin Wirsing on the Occasion of His Retirement from the Chair of Programming and Software Engineering, 8950, Springer, pp.30-45, 2015, Lecture Notes in Computer Science, ⟨10.1007/978-3-319-15545-6_5⟩
Chapitre d'ouvrage hal-01127966v1
Image document

Revisiting Enumerative Instantiation

Andrew J Reynolds , Haniel Barbosa , Pascal Fontaine
[Research Report] University of Iowa; Inria. 2018
Rapport hal-01744956v1
Image document

Scalable Fine-Grained Proofs for Formula Processing

Haniel Barbosa , Jasmin Christian Blanchette , Pascal Fontaine
[Research Report] Universite de Lorraine, CNRS, Inria, LORIA, Nancy, France; Universidade Federal do Rio Grande do Norte, Natal, Brazil; Vrije Universiteit Amsterdam, Amsterdam, The Netherlands; Max-Planck-Institut für Informatik, Saarbrücken, Germany. 2017, pp.25
Rapport hal-01526841v1
Image document

Congruence Closure with Free Variables

Haniel Barbosa , Pascal Fontaine , Andrew Reynolds
[Research Report] Inria, Loria, Universite de Lorraine, UFRN, University of Iowa. 2017
Rapport hal-01442691v2
Image document

A Gentle Non-Disjoint Combination of Satisfiability Procedures (Extended Version)

Paula Chocron , Pascal Fontaine , Christophe Ringeissen
[Research Report] RR-8529, INRIA. 2014
Rapport hal-00985135v1