When quoting this document, please refer to the following
URN: urn:nbn:de:0030-drops-15590
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

08171.AzizAbdullaParosh.Paper.1559.pdf (0.1 MB)


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

  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 =		{},
  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