Certification of Programs involving memory sharing and side effects

The goal is to propose new theoretical bases for proving programs involving memory sharing and side effects (typically, pointer programs in C, objects in OO languages, records with mutable fields
in ML).
There are three different levels of studies: extensions of specification languages with appropriate notions of invariants and description of side effects; design of advanced type systems and static analyses for detecting either alias or separation of pointers; design of verification conditions calculi incorporating notions of modules, pointer separation and refinement.

Research activities
  Program proof
  Functional programming
  Object-Oriented Programming

Participants
FILLIÂTRE Jean-Christophe


More information : http://www.lri.fr/cepromi/index.php/Accueil