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

28Citations
Citations of this article
4Readers
Mendeley users who have this article in their library.
Get full text

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. © 2012 Springer-Verlag.

Cite

CITATION STYLE

APA

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

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free