We propose a new approach for automatic verification of programs with dynamic heap manipulation. The method is based on symbolic (backward) reachability analysis using upward-closed sets of heaps w.r.t. an appropriate preorder on graphs. These sets are represented by a finite set of minimal graph patterns corresponding to a set of bad configurations. We define an abstract semantics for the programs which is monotonic w.r.t. the preorder. Moreover, we prove that our analysis always terminates by showing that the preorder is a well-quasi ordering. Our results are presented for the case of programs with 1-next selector. We provide experimental results showing the effectiveness of our approach. © 2008 Springer-Verlag.
CITATION STYLE
Abdulla, P. A., Bouajjani, A., Cederberg, J., Haziza, F., & Rezine, A. (2008). Monotonic abstraction for programs with dynamic memory heaps. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5123 LNCS, pp. 341–354). https://doi.org/10.1007/978-3-540-70545-1_33
Mendeley helps you to discover research relevant for your work.