salle A. Turing CE4
21 June 2012 - 14h00
Combining Interactive and Automated Theorem Proving in Why3
by Jean-Christophe Filliâtre from CNRS / LRI
Abstract: Why3 is a platform for deductive program verification. It features a rich logical language with polymorphism, algebraic data types, and inductive predicates. Why3 provides an extensive library of proof task transformations that can be chained to produce a suitable input for a large set of theorem provers, including SMT solvers, TPTP provers, as well as interactive proof assistants. In this talk, we show how this technology is used to combine interactive and automated theorem provers in, though not limited to, the context of program verification.
