Hans-Jörg Schurr (Veridis Team) will defend his thesis on Friday, 7th October at 3pm at Loria. His thesis is entitled “Stronger SMT Solvers for Proof Assistants: Proofs, Quantifier Simplification, Strategy Schedules”.

Abstract:

This thesis presents three contributions that have the same underlying
motivation: to improve the utility of SMT solvers as backends for proof
assistants. SMT solvers are automated theorem provers that combine
propositional reasoning with theories.  Proof assistants are tools
that empower users to write formally checked proofs. To help the user,
proof assistants can provide automation by integrating with automated
theorem provers.

Proof assistants typically accept only proofs that are constructed in
the trusted kernel of the assistant.  The first contribution addresses
the reconstruction of SMT proofs in a proof assistant.  We present the
Alethe proof format for SMT solvers.  It improves and unifies previous
work on proof generation from SMT solvers.  The vast majority of these
improvements were informed by the experience provided by a concrete effort
of reconstructing Alethe proofs in the proof assistant Isabelle.

SMT problems generated by proof assistants usually really heavily
on quantifiers.  Since SMT solvers excel on quantifier free problems,
they use quantifier instantation to generate quantifier free formulas.
The second contribution improves quantifier instantiation. It is a
unification-based method that augments the problem with shallow quantified
formulas obtained from assertions with nested quantifiers. These
new formulas help unlocking the regular instantiation techniques, but
parsimony is necessary since they might also be misguiding.  The method
allows the solver to prove more formulas, faster.

The heuristics of an SMT solvers can be parameterized.  A specific
parameterization of the entire solver is called a strategy, and the best
strategy usually differs from problem to problem. The third contribution
is a toolbox to work with strategy schedules.  A key component of the
toolbox is a tool that uses integer programming to generate strategy
schedules.  Beyond this tool, the toolbox also contains tools for
simulating and analyzing schedules. We used the toolbox to select
strategies that solve many problems generated by Isabelle.

Jury:

• Directeurs de thèse : Stephan MERZ (Université de Lorraine, Inria), Pascal FONTAINE (Université de Liège), Jasmin BLANCHETTE (Vrije Universiteit Amsterdam)
• Rapporteurs : Frédéric BLANQUI (Université Paris Saclay, Inria), Elaine PIMENTEL (University College London)
• Examinateurs : Chantal KELLER (Université Paris Saclay, LMF), Christophe RINGEISSEN (Université de Lorraine, Inria), Cesare TINELLI (The University of Iowa)