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. © 2012 Springer-Verlag.
CITATION STYLE
Bouajjani, A., Drǎgoi, C., Enea, C., & Sighireanu, M. (2012). Abstract domains for automated reasoning about list-manipulating programs with infinite data. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7148 LNCS, pp. 1–22). https://doi.org/10.1007/978-3-642-27940-9_1
Mendeley helps you to discover research relevant for your work.