Shape Analysis via Monotonic Abstraction

Authors Parosh Aziz Abdulla, Ahmed Bouajjani, Jonathan Cederberg, Frédéric Haziza, Ran Ji, Ahmed Rezine



PDF
Thumbnail PDF

File

DagSemProc.08171.3.pdf
  • Filesize: 153 kB
  • 11 pages

Document Identifiers

Author Details

Parosh Aziz Abdulla
Ahmed Bouajjani
Jonathan Cederberg
Frédéric Haziza
Ran Ji
Ahmed Rezine

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

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)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail