Andrei Paskevich

Abstract

This lecture is an introduction to deductive program verification using the Why3 tool (http://why3.lri.fr/). Why3 provides a programming language with specification annotations, type polymorphism, mutable data types, algebraic data types, pattern matching, and exceptions. It allows us to verify annotated programs using automated and interactive theorem provers like Alt-Ergo, CVC4, Z3, Coq, and many others. This lecture introduces elementary concepts and techniques of deductive verification: pre- and postconditions, loop invariants, weakest precondition calculus, termination proofs, ghost code, modeling of data structures, etc. We discuss in detail how Why3 leverages its type system for program verification - notably to infer the ghost status of program expressions and to track aliases between mutable values.

Andrei's material is here: http://why3.lri.fr/eutypes-2017