Vendredi 2 Décembre

Retour à la vue des calendrier
Vendredi 2 Décembre
Heure: 14:00 - 15:00
Lieu: Salle B107, bâtiment B, Université de Villetaneuse
Résumé: Proving array-manipulating programs without arrays
Description: David Monniaux Automatically verifying safety properties of programs is hard. Many
approaches exist for verifying programs operating on Boolean and integer
values (e.g. abstract interpretation, counterexample-guided abstraction
refinement using interpolants), but transposing them to array properties has
been fraught with difficulties.
Our work addresses that issue with a powerful and flexible abstraction that
morphes concrete array cells into a finite set of abstract ones. This
abstraction is parametric both in precision and in the back-end analysis used.

One possible application would be distributed systems, where processes
are modeled using arrays indexed by the process ID.