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.06081.5
URN: urn:nbn:de:0030-drops-7284
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2006/728/
Go to the corresponding Portal

Beyer, Dirk ; Henzinger, Thomas A. ; Théoduloz, Grégory

Lazy Shape Analysis

pdf-format:
06081.BeyerDirk.Paper.728.pdf (0.4 MB)

Abstract

Many software model checkers are based on predicate abstraction. If
the verification goal depends on pointer structures, the approach does
not work well, because it is difficult to find adequate predicate
abstractions for the heap. In contrast, shape analysis, which uses
graph-based heap abstractions, can provide a compact representation of
recursive data structures. We integrate shape analysis into the
software model checker BLAST. Because shape analysis is expensive, we
do not apply it globally. Instead, we ensure that, like predicates,
shape graphs are computed and stored locally, only where necessary for
proving the verification goal. To achieve this, we extend lazy
abstraction refinement, which so far has been used only for predicate
abstractions, to three-valued logical structures. This approach does
not only increase the precision of model checking, but it also
increases the efficiency of shape analysis. We implemented the
technique by extending BLAST with calls to TVLA.


BibTeX - Entry

@InProceedings{beyer_et_al:DagSemProc.06081.5,
  author =	{Beyer, Dirk and Henzinger, Thomas A. and Th\'{e}oduloz, Gr\'{e}gory},
  title =	{{Lazy Shape Analysis}},
  booktitle =	{Software Verification: Infinite-State Model Checking and Static Program Analysis},
  pages =	{1--16},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6081},
  editor =	{Parosh Aziz Abdulla and Ahmed Bouajjani and Markus M\"{u}ller-Olm},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2006/728},
  URN =		{urn:nbn:de:0030-drops-7284},
  doi =		{10.4230/DagSemProc.06081.5},
  annote =	{Keywords: Software model checking, Shape analysis, Counterexample-guided abstraction refinement, Interpolation, Predicate abstraction}
}

Keywords: Software model checking, Shape analysis, Counterexample-guided abstraction refinement, Interpolation, Predicate abstraction
Collection: 06081 - Software Verification: Infinite-State Model Checking and Static Program Analysis
Issue Date: 2006
Date of publication: 09.11.2006

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