|
|
 |
|
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. |
|
|
