Sökning: onr:"swepub:oai:DiVA.org:uu-106059" >
Monotonic abstracti...
Monotonic abstraction for programs with dynamic memory heaps
-
- Abdulla, Parosh Aziz (författare)
- Uppsala universitet,Datorteknik
-
Bouajjani, Ahmed (författare)
-
- Cederberg, Jonathan (författare)
- Uppsala universitet,Datorteknik
-
visa fler...
-
- Haziza, Frédéric (författare)
- Uppsala universitet,Datorteknik
-
- Rezine, Ahmed (författare)
- Uppsala universitet,Datorteknik
-
visa färre...
-
(creator_code:org_t)
- Berlin : Springer-Verlag, 2008
- 2008
- Engelska.
-
Serie: Technical report / Department of Information Technology, Uppsala University, 1404-3203 ; 2008-015
-
Ingår i: Computer Aided Verification. - Berlin : Springer-Verlag. ; , s. 341-354
- Relaterad länk:
-
https://link.springe...
-
visa fler...
-
https://urn.kb.se/re...
-
https://doi.org/10.1...
-
https://urn.kb.se/re...
-
visa färre...
Abstract
Ämnesord
Stäng
- 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.
Ämnesord
- NATURVETENSKAP -- Data- och informationsvetenskap -- Datavetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences -- Computer Sciences (hsv//eng)
Nyckelord
- Computer science
- Datavetenskap
Publikations- och innehållstyp
- ref (ämneskategori)
- kon (ämneskategori)