Consider participating to the following events:

• IJCAR 2018
• SMT 2018
• SC² 2018
• The SAT/SMT/AR summer school 2018

If you have strong motivations to work as an Internship Student, PhD Student, or as a PostDoc in our team, e.g. on SMT or verification of distributed systems, please us as soon as possible.

Address

LORIA
Équipe VeriDis, Bât B
615, rue du Jardin Botanique
F-54602 Villers-lès-Nancy
France

Office

B 262 (second floor)

Email

Phone

+33 354 95 84 78

Fax

+33 383 41 30 79

Interests (Research)

Verification of distributed systems
Automated theorem proving
Cooperation of deduction tools
Satisfiability Modulo Theories
Combination of theories

Bibtex abbreviations used in the bib files below


• Andrew Reynolds, Haniel Barbosa, and Pascal Fontaine. Revisiting Enumerative Instantiation. In Dirk Beyer and Marieke Huisman, editors, Tools and Algorithms for Construction and Analysis of Systems (TACAS), Lecture Notes in Computer Science, 2018. to appear.
  bibtex
• Haniel Barbosa, Pascal Fontaine, and Andrew Reynolds. Congruence closure with free variables. In Axel Legay and Tiziana Margaria, editors, Tools and Algorithms for Construction and Analysis of Systems (TACAS), volume 10206 of Lecture Notes in Computer Science, pages 214-230, 2017.
  Preprint: pdf bibtex
• Haniel Barbosa, Jasmin Christian Blanchette, and Pascal Fontaine. Scalable fine-grained proofs for formula processing. In Leonardo de Moura, editor, Proc. Conference on Automated Deduction (CADE), volume 10395 of Lecture Notes in Computer Science, pages 398-412. Springer, 2017.
  Preprint: pdf bibtex
• Pascal Fontaine, Mizuhito Ogawa, Thomas Sturm, and Xuan-Tung Vu. Subtropical satisfiability. In Clare Dixon and Marcelo Finger, editors, Frontiers of Combining Systems (FroCoS), volume 10483 of Lecture Notes in Computer Science, pages 189-206. Springer, 2017.
  Preprint: pdf bibtex
• Andreas Fellner, Pascal Fontaine, and Bruno Woltzenlogel Paleo. NP-completeness of small conflict set generation for congruence closure. Formal Methods in System Design, 51(3):533-544, December 2017.
  Preprint: pdf bibtex
• 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, and Thomas Sturm. SC^2: Satisfiability checking meets symbolic computation - (project paper). In Michael Kohlhase, Moa Johansson, Bruce R. Miller, Leonardo de de Moura, and Frank Wm. Tompa, editors, Intelligent Computer Mathematics (CICM), volume 9791 of Lecture Notes in Computer Science, pages 28-43. Springer, 2016.
  Preprint: pdf bibtex
• Carlos Areces, Pascal Fontaine, and Stephan Merz. Modal satisfiability via SMT solving. In Rocco De Nicola and Rolf Hennicker, editors, Software, Services and Systems. Essays Dedicated to Martin Wirsing on the Occasion of His Emeritation, volume 8950 of Lecture Notes in Computer Science, pages 30-45. Springer, 2015.
  Preprint: pdf bibtex
• Paula Chocron, Pascal Fontaine, and Christophe Ringeissen. A rewriting approach to the combination of data structures with bridging theories. In Carsten Lutz and Silvio Ranise, editors, Frontiers of Combining Systems (FroCoS), volume 9322 of Lecture Notes in Computer Science, pages 275-290. Springer, 2015.
  Preprint: pdf bibtex
• Paula Chocron, Pascal Fontaine, and Christophe Ringeissen. A polite non-disjoint combination method: Theories with bridging functions revisited. In Amy P. Felty and Aart Middeldorp, editors, Proc. Conference on Automated Deduction (CADE), volume 9195 of Lecture Notes in Computer Science, pages 419-433. Springer, 2015.
  Preprint: pdf bibtex
• Andreas Fellner, Pascal Fontaine, Georg Hofferek, and Bruno Woltzenlogel Paleo. NP-completeness of small conflict set generation for congruence closure. In Vijay Ganesh and Dejan Jovanović, editors, International Workshop on Satisfiability Modulo Theories (SMT), 2015.
  Preprint: bibtex
• Maximilian Jaroschek, Pablo Federico Dobal, and Pascal Fontaine. Adapting real quantifier elimination methods for conflict set computation. In Carsten Lutz and Silvio Ranise, editors, Frontiers of Combining Systems (FroCoS), volume 9322 of Lecture Notes in Computer Science, pages 151-166. Springer, 2015.
  Preprint: pdf bibtex
• Paula Chocron, Pascal Fontaine, and Christophe Ringeissen. A gentle non-disjoint combination of satisfiability procedures. In Stéphane Demri, Deepak Kapur, and Christoph Weidenbach, editors, International Joint Conference on Automated Reasoning (IJCAR), volume 8562 of LNCS. pages 122--136, Springer, 2014.
  Preprint: pdf bibtex
• David Déharbe, Pascal Fontaine, Yoann Guyot and Laurent Voisin. Integrating SMT solvers in Rodin. In John Derrick, John A. Fitzgerald, Stefania Gnesi, Sarfraz Khurshid, Michael Leuschel, Steve Reeves and Elvinia Riccobene, editors, volume 94 of Science of Computer Programming. pages 130--143, 2014.
  Preprint: pdf bibtex
• Paula Chocron, Pascal Fontaine, and Christophe Ringeissen. Satisfiability modulo non-disjoint combinations of theories connected via bridging functions. In Silvio Ghilardi, Ulrike Sattler, and Viorica Sofronie-Stokkermans, editors, Automated Deduction: Decidability, Complexity, Tractability (ADDCT), 2014.
  Preprint: pdf bibtex
• Clark Barrett, Leonardo de Moura, and Pascal Fontaine. Proofs in satisfiability modulo theories. In All about Proofs, Proofs for All (APPA), 2014.
  Preprint: pdf bibtex
• David Déharbe, Pascal Fontaine, Daniel Le Berre and Bertrand Mazure. Computing prime implicants. Formal Methods in Computer-Aided Design (FMCAD), IEEE. pages 46-62, 2013.
  Preprint: pdf bibtex
• Carlos Areces, David Déharbe, Pascal Fontaine and Ezequiel Orbe. SyMT: finding symmetries in SMT formulas, Proc. Workshop on Satisfiability Modulo Theories (SMT), 2013.
  Preprint: pdf bibtex
• Diego Caminha B. de Oliveira, David Déharbe and Pascal Fontaine. Combining decision procedures by (model-)equality propagation. Science of Computer Programming, 77(4): 518-532 (2012).
  Preprint: pdf bibtex
• David Déharbe, Pascal Fontaine, Yoann Guyot and Laurent Voisin. SMT solvers for Rodin. In John Derrick, John A. Fitzgerald, Stefania Gnesi, Sarfraz Khurshid, Michael Leuschel, Steve Reeves and Elvinia Riccobene, editors, In Proc. ABZ, volume 7316 of LNCS. pages 194-207, Springer, 2012.
  Preprint: pdf bibtex
• Pascal Fontaine, Stephan Merz and Christoph Weidenbach. Combination of Disjoint Theories: Beyond Decidability. In Bernhard Gramlich, Dale Miller, Uli Sattler, editors, In Proc. International Joint Conference on Automated Reasoning (IJCAR), volume 7364 of LNCS. pages 256-270, Springer, 2012.
  Preprint: pdf bibtex
• Carlos Areces and Pascal Fontaine. Combining Theories: The Ackerman and Guarded Fragments. In Cesare Tinelli and Viorica Sofronie-Stokkermans, editors, In Proc. Frontiers of Combining Systems (FroCoS), volume 6989 of LNCS. pages 40--54, Springer-Verlag, 2011.
  Preprint: pdf bibtex
  
• David Déharbe, Pascal Fontaine and Bruno Woltzenlogel Paleo. Quantifier Inference Rules for SMT proofs. Workshop on Proof eXchange for Theorem Proving (PxTP), 2011.
  Preprint: pdf bibtex
  
• Frédéric Besson, Pascal Fontaine and Laurent Théry A Flexible Proof Format for SMT: a Proposal. Workshop on Proof eXchange for Theorem Proving (PxTP), 2011.
  Preprint: pdf bibtex
  
• David Déharbe, Pascal Fontaine, Stephan Merz and Bruno Woltzenlogel Paleo. Exploiting symmetry in SMT problems. In Nikolaj Bjørner and Viorica Sofronie-Stokkermans, editors, In Proc. Conference on Automated Deduction (CADE), volume 6803 of LNCS. pages 222--236, Springer-Verlag, 2011.
  Preprint: pdf bibtex
  Long version: pdf bibtex
• Pascal Fontaine, Stephan Merz and Bruno Woltzenlogel Paleo. Compression of Propositional Resolution Proofs via Partial Regularization. In Nikolaj Bjørner and Viorica Sofronie-Stokkermans, editors, In Proc. Conference on Automated Deduction (CADE), volume 6803 of LNCS. pages , Springer-Verlag, 2011.
  Preprint: pdf bibtex
  
• Pascal Fontaine, Stephan Merz and Bruno Woltzenlogel Paleo. Exploring and Exploiting Algebraic and Graphical Properties of Resolution. In Aarti Gupta and Daniel Kroening editors In Proc. Workshop on Satisfiability Modulo Theories (SMT), 2010.
  Preprint: pdf bibtex
• Thomas Bouton, Diego Caminha B. de Oliveira, David Déharbe and Pascal Fontaine. GridTPT: a distributed platform for Theorem Prover Testing. In Boris Konev, Renate Schmidt and Stephan Schulz, editors, In Proc. Workshop on Practical Aspects of Automated Reasoning 2010.
  Preprint: pdf bibtex
• Pascal Fontaine. Combinations of theories for decidable fragments of first-order logic. In Silvio Ghilardi and Roberto Sebastiani, editors, In Proc. Frontiers of Combining Systems (FroCoS), Trento, volume 5749 of LNCS, pages 263--278. Springer-Verlag, 2009.
  Preprint: pdf bibtex
• Thomas Bouton, Diego Caminha B. de Oliveira, David Déharbe and Pascal Fontaine. veriT: an open, trustable and efficient SMT-solver. In Renate A. Schmidt, editor, In Proc. Conference on Automated Deduction (CADE), volume 5663 of LNCS, pages 151--156. Springer-Verlag, 2009.
  Preprint: pdf bibtex
• Diego Caminha B. de Oliveira and David Déharbe and Pascal Fontaine. Combining decision procedures by (model-)equality propagation. In P. Machado, A. Andrade and A. Duran, editors, In Proc. of the Brazilian Symposium on Formal Methods (SBMF), Salvador, Bahia, Brazil, 2008. volume 240 of Electr. Notes Theor. Comput. Sci., pages 113-128, 2009
  Preprint: pdf bibtex
• Pascal Fontaine. Combinations of Theories and the Bernays-Schönfinkel-Ramsey Class. In Bernhard Beckert, editor, In Proc. 4th International Verification Workshop - VERIFY'07, Bremen, 2007.
  Preprint: pdf postscript bibtex slides
• Clément Hurlin, Amine Chaieb, Pascal Fontaine, Stephan Merz and Tjark Weber. Practical Proof Reconstruction for First-order Logic and Set-Theoretical Constructions. In Lucas Dixon and Moa Johansson, editors, In Proc. of The Isabelle Workshop 2007, Bremen, 2007.
  Preprint: pdf bibtex
• Diego Caminha B. de Oliveira and David Déharbe and Pascal Fontaine. haRVey: satisfaisabilité et théories (Présentation d'outil). Marie-Laure Potet, Pierre-Yves Schobbens, Hubert Toussaint et Germain Saval éditeurs, Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL), 2007.
  Preprint: pdf bibtex
• David Déharbe, Pascal Fontaine, Silvio Ranise and Christophe Ringeissen. Decision procedures for the formal analysis of software (Extended Abstract) . In Kamel Barkaoui, Ana Cavalcanti and Antonio Cerone, editors, In Proc. International Colloquium on Theoretical Aspects of Computing (ICTAC), volume 4281 of LNCS, pages 366--370. Springer-Verlag, 2006.
  Preprint: pdf bibtex
• David Déharbe and Pascal Fontaine. haRVey: combining reasoners. In Stephan Merz and Tobias Nipkow, editors, In Proc. Sixth International Workshop on Automated Verification of Critical Systems (AVOCS), 2006.
  Preprint: pdf bibtex
• Pascal Fontaine, Jean-Yves Marion, Stephan Merz, Leonor Prensa Nieto and Alwen Tiu. Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants. In Holger Hermanns and Jens Palsberg, editors, In Proc. Tools and Algorithm for the Construction and Analysis of Systems (TACAS), volume 3920 of LNCS, pages 167--181. Springer-Verlag, 2006.
  Preprint: pdf bibtex
• Pascal Fontaine, Kamal Gupta, Jean-Yves Marion, Stephan Merz, Leonor Prensa Nieto and Alwen Tiu. Towards a Combination of Heterogeneous Deductive Tools for System Verification: A Case Study on Clock Synchronization. Workshop on Applied Semantics (APPSEM), September 2005, Frauenchiemsee, Germany.
• Pascal Fontaine, Silvio Ranise, and Calogero G. Zarba. Combining lists with non-stably infinite theories. In Franz Baader and Andrei Voronkov, editors, In Proc. Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), volume 3452 of LNCS, pages 51--66. Springer-Verlag, 2005.
  Preprint: pdf postscript bibtex
• Pascal Fontaine and Pascal Gribomont. Combining non-stably infinite, non-first order theories. In W. Ahrendt, P. Baumgartner, H. de Nivelle, S. Ranise and C. Tinelli editors, Selected Papers from the Workshops on Disproving and the Second International Workshop on Pragmatics of Decision Procedures (PDPAR 2004), volume 125, issue 3 of ENTCS, pages 37-51, 2005.
  Preprint: pdf postscript bibtex
• Pascal Fontaine. Techniques for verification of concurrent systems with invariants. PhD Thesis, Institut Montefiore, Université de Liège, Belgium, September 2004.
  postscript postscript (2/sheet) bibtex slides
  
• Pascal Fontaine and E. Pascal Gribomont. Decidability of invariant validation for parameterised systems. In Hubert Garavel and John Hatcliff, editors, Proc. Tools and Algorithms for Construction and Analysis of Systems (TACAS), volume 2619 of LNCS, pages 97--112. Springer-Verlag, 2003.
  Preprint: pdf postscript bibtex
• Pascal Fontaine and E. Pascal Gribomont. Using BDDs with Combinations of Theories. In Proc. Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), volume 2514 of LNCS, pages 190--201. Springer-Verlag, 2002.
  Preprint: pdf postscript bibtex
• Pascal Fontaine, E. Pascal Gribomont et Nachaat Salloum. Spécification et vérification par CAVEAT d'un système de contrôle d'accès. Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL), pages 173--187, janvier 2000.