Consider submitting and participating to the following events:

• PAAR 2012
• PxTP 2012
• SMT 2012

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

Internet mail is an asynchronous and unreliable communication medium.
Please consider using phone for important and/or urgent messages.

Phone

+33 354 95 84 78

Fax

+33 383 41 30 79

Interests (Research)

Verification of distributed algorithms
Cooperation of deduction tools
Satisfiability Modulo theories
Combination of theories

Thesis

• 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
  

Papers

• 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
  
• Diego Caminha B. de Oliveira, David Déharbe and Pascal Fontaine. Combining decision procedures by (model-)equality propagation. Science of Computer Programming, 2011. To Appear.
  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 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.