License
When quoting this document, please refer to the following
URN: urn:nbn:de:0030-drops-15590
URL: http://drops.dagstuhl.de/opus/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:
Document 1.pdf (153 KB)


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:DSP:2008:1559,
  author =	{Parosh Aziz Abdulla and Ahmed Bouajjani and Jonathan Cederberg and Fr{\'e}d{\'e}ric Haziza and Ran Ji and Ahmed Rezine},
  title =	{Shape Analysis via Monotonic Abstraction},
  booktitle =	{Beyond the Finite: New Challenges in Verification and Semistructured Data},
  year =	{2008},
  editor =	{Anca Muscholl and Ramaswamy Ramanujam and Micha{\"e}l Rusinowitch and Thomas Schwentick and Victor Vianu},
  number =	{08171},
  series =	{Dagstuhl Seminar Proceedings},
  ISSN =	{1862-4405},
  publisher =	{Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2008/1559},
  annote =	{Keywords: Shape analysis, Program verification, Static analysis}
}

Keywords: Shape analysis, Program verification, Static analysis
Seminar: 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 Published by LZI