|Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data|
du groupe Modélisation et Verification
|Date|| 2012-02-09 11:30-12:30|
|Titre||Abstract 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. |
|Lieu||Salle 076, LaBRI, Rez-de-chaussée |
|Orateur||Cezara Dragoi |
|Url||IST Austria |
Aucun document lié à cet événement.RetourRetour à l'index