Pascal Fontaine (Mosel-Veridis) will defend his habilitation on Monday, October 8th at 3PM in room C005.

His presentation is entitled “Satisfiability Modulo Theories”.

Abstract: Satisfiability Modulo Theories (SMT) is an automatic reasoning paradigm to check the satisfiability of logic formulas in presence of predicates and functions interpreted within a theory.  Among  relevant theories, one finds the empty theory (uninterpreted symbols), various arithmetic theories, and theories for data-types, sets,… SMT solvers generally also implement some kind of combination of theories, so that they can handle formulas containing interpreted symbols from several of those theories at the same time.  My previous contributions as well as my project revolve around SMT, mainly on decision procedures, combination of theories and quantifier handling for SMT.  My main directions for future research are to extend SMT to handle higher-order formulas, and to further improve efficiency, quantifier handling, and proof production for SMT.  A last aspect of my work involves applying SMT techniques for verification, more particularly for TLA+ and the B method.

Committee:
Sylvain Conchon, Université Paris-Sud 11, France
Stephan Merz, Université de Lorraine, CNRS, Inria, Loria, France
Renate Schmidt, University of Manchester, UK
Roberto Sebastiani, Università di Trento, Italy
Jeanine Souquières, Université de Lorraine, CNRS, Loria, France
Viorica Sofronie-Stokkermans, Universität Koblenz-Landau, Germany
Cesare Tinelli, The University of Iowa, USA