License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/DagSemProc.08171.3
URN: urn:nbn:de:0030-drops-15590
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2008/1559/
Go to the corresponding Portal

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

Shape Analysis via Monotonic Abstraction

pdf-format:
08171.AzizAbdullaParosh.Paper.1559.pdf (0.1 MB)

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.

BibTeX - Entry

@InProceedings{azizabdulla_et_al:DagSemProc.08171.3,
  author =	{Aziz Abdulla, Parosh and Bouajjani, Ahmed and Cederberg, Jonathan and Haziza, Fr\'{e}d\'{e}ric and Ji, Ran and Rezine, Ahmed},
  title =	{{Shape Analysis via Monotonic Abstraction}},
  booktitle =	{Beyond the Finite: New Challenges in Verification and Semistructured Data},
  pages =	{1--11},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2008},
  volume =	{8171},
  editor =	{Anca Muscholl and Ramaswamy Ramanujam and Micha\"{e}l Rusinowitch and Thomas Schwentick and Victor Vianu},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2008/1559},
  URN =		{urn:nbn:de:0030-drops-15590},
  doi =		{10.4230/DagSemProc.08171.3},
  annote =	{Keywords: Shape analysis, Program verification, Static analysis}
}

Keywords: Shape analysis, Program verification, Static analysis
Collection: 08171 - Beyond the Finite: New Challenges in Verification and Semistructured Data
Issue Date: 2008
Date of publication: 23.07.2008

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI