Le séminaire du LSV

Le séminaire du LSV a lieu le mardi à 11h00. Le lieu habituel est la salle de conférences au Pavillon des Jardins (plan d'accès). Pour être informé par email des prochains séminaires, contacter Stéphane Le Roux and Matthias Fuegger.

Le séminaire du LSV est public et ne nécessite aucune inscription préalable.

Séminaires passés

Automatic verification of heap-manipulating sequential programs with unbounded data

Visiter le site web pour cet événement | Exporter cet événement au format iCalendar

 Cezara Drăgoi
Date
Le mardi 20 mars 2012 à 11:00
Lieu
Salle de Conférence (Pavillon des Jardins)
Orateur
Cezara Drăgoi (IST Austria)

We develop a logic-based framework for the automatic verification of sequential programs manipulating dynamic data structures carrying unbounded data. We are interested in proving safety specifications, that describe the structure of the allocated memory, its size and also the values of the data fields. To this we have considered a framework where sets of configurations are represented by formulas in first order logic with reachability predicates.

First, we investigated the automation of pre/post-condition reasoning. We introduced a multi-sorted first order logic that has a decidable satisfiability problem and it is closed under the computation of the strongest post-condition. This logic combines reachability predicates that are used to describe the structure of the allocated memory, linear constraints to describe its size and formulas in a first order logic over the data domain to constrain the values of the data fields.

Second, to increase the level of automation we address the issue of synthesizing assertions for programs with singly-linked lists. These assertions represent over-approximations of the program's set of reachable states. We define an abstract interpretation based framework which combines a specific finite-range abstraction on the structure of the allocated memory with an abstract domain on sequences of data.


À propos du LSV

Agenda des séminaires

Exporter l'agenda au format iCalendar | Les séminaires précédents

mar. 19 février

Les séminaires précédents