Evènement pour le groupe Modélisation et Verification

Date 2012-02-09  11:30-12:30
TitreAbstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data 
RésuméWe introduce a framework based on abstract interpretation for reasoning about programs with lists carrying integer numerical data. In this framework, abstract domains are used to describe and manipulate complex constraints on configurations of these programs mixing constraints on the shape of the heap, sizes of the lists, and on the data stored in the lists. We consider a domain where data is described by formulas in a universally quantified fragment of the first-order logic over sequences, as well as a domain where data is described using constrains on the multisets of data in the lists. Moreover, we provide powerful techniques for automatic validation of Hoare-triples and invariant checking, as well as for automatic synthesis of invariants and procedure summaries using modular inter-procedural analysis. The approach has been implemented in a tool called CELIA and experimented successfully on a large benchmark of programs.  
LieuSalle 076, LaBRI, Rez-de-chaussée 
OrateurCezara Dragoi 
UrlIST Austria  

Aucun document lié à cet événement.

Retour à l'index