TY - GEN
T1 - Abstract domains for automated reasoning about list-manipulating programs with infinite data
AU - Bouajjani, Ahmed
AU - Drǎgoi, Cezara
AU - Enea, Constantin
AU - Sighireanu, Mihaela
PY - 2012/1/30
Y1 - 2012/1/30
N2 - 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.
AB - 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.
UR - https://www.scopus.com/pages/publications/84856179511
U2 - 10.1007/978-3-642-27940-9_1
DO - 10.1007/978-3-642-27940-9_1
M3 - Conference contribution
AN - SCOPUS:84856179511
SN - 9783642279393
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 1
EP - 22
BT - Verification, Model Checking, and Abstract Interpretation - 13th International Conference, VMCAI 2012, Proceedings
T2 - 13th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2012
Y2 - 22 January 2012 through 24 January 2012
ER -