Abstract domains for automated reasoning about list manipulating programs with infinite data Conference Paper


Author(s): Bouajjani, Ahmed; Drǎgoi, Cezara; Enea, Constantin; Sighireanu, Mihaela
Title: Abstract domains for automated reasoning about list manipulating programs with infinite data
Title Series: LNCS
Affiliation IST Austria
Abstract: We describe a framework for reasoning about programs with lists carrying integer numerical data. We use abstract domains to describe and manipulate complex constraints on configurations of these programs mixing constraints on the shape of the heap, sizes of the lists, on the multisets of data stored in these lists, and on the data at their different positions. 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.
Keywords: Abstract domains; Automatic synthesis; Automated reasoning; Automatic validation; Inter-procedural analysis; Invariant checking; Multi-sets; Numerical data
Conference Title: VMCAI: Verification, Model Checking and Abstract Interpretation
Volume: 7148
Conference Dates: January 22-24, 2012
Conference Location: Philadelphia, PA, USA
Publisher: Springer  
Location: Berlin, Germany
Date Published: 2012-02-26
Start Page: 1
End Page: 22
Sponsor: This work was partly supported by the French National Research Agency (ANR) project Veridyc (ANR-09-SEGI-016).
DOI: 10.1007/978-3-642-27940-9_1
Open access: no
IST Austria Authors
Related IST Austria Work