DagSemProc.08171.3.pdf
- Filesize: 153 kB
- 11 pages
Document
Shape Analysis via Monotonic Abstraction
Authors
-
Part of:
Volume:
Dagstuhl Seminar Proceedings, Volume 8171
Series: Dagstuhl Seminar Proceedings (DagSemProc) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2008-07-23
Cite AsGet BibTex
Parosh Aziz Abdulla, Ahmed Bouajjani, Jonathan Cederberg, Frédéric Haziza, Ran Ji, and Ahmed Rezine. Shape Analysis via Monotonic Abstraction. In Beyond the Finite: New Challenges in Verification and Semistructured Data. Dagstuhl Seminar Proceedings, Volume 8171, pp. 1-11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2008)
https://doi.org/10.4230/DagSemProc.08171.3
https://doi.org/10.4230/DagSemProc.08171.3
Abstract
We propose a new formalism for reasoning about dynamic memory heaps, using monotonic abstraction and symbolic backward reachability analysis. We represent the heaps as graphs, and introduce an ordering on these graphs. This enables us to represent the violation of a given safety property as the reachability of a finitely representable set of bad graphs. We also describe how to symbolically compute the reachable states in the transition system induced by a program.
Keywords
- Shape analysis
- Program verification
- Static analysis
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads