Français Anglais
Accueil Annuaire Plan du site
Research results
Contract / grant for group Toccata
CEPROMI

Subvention
Mar 2008 - Dec 2009

Group : Toccata
Principal investigator : MARCHÉ Claude

Administrator : 
Affiliation : INRIA

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
Contracts & grants
° SESAME DIGIPODS UPS
REMOTE COLLABORATIVE INTERACTION AMONG HETEROGENEOUS VISUALIZATION PLATFORMS
REGION IDF

° NEXT
NEXT