LSV Seminar
The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
Past Seminars
Automatic verification of heap-manipulating sequential programs with unbounded data
- Date
- Tuesday, March 20 2012 at 11:00AM
- Place
- Salle de Conférence (Pavillon des Jardins)
- Speaker
- 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.