DROPS

Document

Evaluating Software Verification Systems: Benchmarks and Competitions (Dagstuhl Reports 14171)

Authors: Dirk Beyer, Marieke Huisman, Vladimir Klebanov, and Rosemary Monahan

Published in: Dagstuhl Reports, Volume 4, Issue 4 (2014)

Abstract

This report documents the program and the outcomes of Dagstuhl Seminar 14171 "Evaluating Software-Verification Systems: Benchmarks and Competitions". The seminar brought together a large group of current and future competition organizers and participants, benchmark maintainers, as well as practitioners and researchers interested in the topic. The seminar was conducted as a highly-interactive event, with a wide spectrum of contributions from participants, including talks, tutorials, posters, tool demstrations, hands-on sessions, and a live competition.

Cite as

Dirk Beyer, Marieke Huisman, Vladimir Klebanov, and Rosemary Monahan. Evaluating Software Verification Systems: Benchmarks and Competitions (Dagstuhl Reports 14171). In Dagstuhl Reports, Volume 4, Issue 4, pp. 1-19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)

Copy BibTex To Clipboard

@Article{beyer_et_al:DagRep.4.4.1,
  author =	{Beyer, Dirk and Huisman, Marieke and Klebanov, Vladimir and Monahan, Rosemary},
  title =	{{Evaluating Software Verification Systems: Benchmarks and Competitions (Dagstuhl Reports 14171)}},
  pages =	{1--19},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2014},
  volume =	{4},
  number =	{4},
  editor =	{Beyer, Dirk and Huisman, Marieke and Klebanov, Vladimir and Monahan, Rosemary},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.4.4.1},
  URN =		{urn:nbn:de:0030-drops-46157},
  doi =		{10.4230/DagRep.4.4.1},
  annote =	{Keywords: Formal Verification, Deductive Verification, Automatic Verification, Theorem Proving, Model Checking, Program Analysis, Competition, Comparative Eval}
}

Document

DOI: 10.4230/DagSemProc.06081.5

Lazy Shape Analysis

Authors: Dirk Beyer, Thomas A. Henzinger, and Grégory Théoduloz

Published in: Dagstuhl Seminar Proceedings, Volume 6081, Software Verification: Infinite-State Model Checking and Static Program Analysis (2006)

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.

Cite as

Dirk Beyer, Thomas A. Henzinger, and Grégory Théoduloz. Lazy Shape Analysis. In Software Verification: Infinite-State Model Checking and Static Program Analysis. Dagstuhl Seminar Proceedings, Volume 6081, pp. 1-16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@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/entities/document/10.4230/DagSemProc.06081.5},
  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}
}

Search Results

Documents authored by Beyer, Dirk

Evaluating Software Verification Systems: Benchmarks and Competitions (Dagstuhl Reports 14171)

Abstract

Cite as

Lazy Shape Analysis

Abstract

Cite as

Thanks for your feedback!

Could not send message