Monotonic abstraction for programs with dynamic memory heaps
2008 (English)In: Computer Aided Verification / [ed] Gupta A, Malik S, Berlin: Springer-Verlag , 2008, 341-354 p.Conference paper (Refereed)
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.
Place, publisher, year, edition, pages
Berlin: Springer-Verlag , 2008. 341-354 p.
, Lecture Notes in Computer Science, ISSN 0302-9743 ; 5123
IdentifiersURN: urn:nbn:se:uu:diva-106059DOI: 10.1007/978-3-540-70545-1_33ISI: 000257539900033OAI: oai:DiVA.org:uu-106059DiVA: diva2:223663
20th International Conference on Computer Aided Verification Princeton, NJ, JUL 07, 2008