Deductive program verification in Why3 (miniworkshop)

Jean-Christophe Filliatre

Laboratoire de Recherche en Informatique (LRI)
Universit Paris Sud 11

Tuesday, 15 January, 11.00 (note the unusual weekday and time)
Cybernetica Bldg (Akadeemia tee 21), room B101

Webpage for this miniworkshop

Abstract: Why3 is the next generation of the Why software verification platform. Why3 clearly separates the purely logical specification part from generation of verification conditions for programs. Regarding the former, Why3 comes with a new enhanced language of logical specification. It features a rich 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. Regarding the latter, Why3 comes with a powerful programming language featuring recursive functions, local bindings, pattern matching, exceptions, and records with possibly mutable fields. Aliasing are excluded by type checking to allow the computation of natural verification conditions through a weakest precondition calculus.

J.-C. Filliatre's visit is partially funded by Institut Francais Estonie and partially by EXCS.

Tarmo Uustalu
Last update 12 January 2013