Claude Marché,
INRIA Saclay - Île-de-France

Deductive verification of pointer programs: the Why/Krakatoa approach

Abstract

We present the Why/Krakatoa approach to deductive verification. This includes the following topics: 1) The Why VC generator for alias-free programs: WP calculus with native support for exceptions, 2) Modeling heap memory of pointer programs by translation into Why, illustration on modeling JavaCard persistent memory, 3) Specifying program behaviors using algebraic datatypes, 4) Integration of static analyses techniques: non-null policy, memory separation, synthesis of annotations.

Information from the lecturer: Please read this webpage for Why/Krakatoa installation instructions (new version 2.18) and the course material.