License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.TrustworthySW.2006.701
URN: urn:nbn:de:0030-drops-7016
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2006/701/
Go to the corresponding OASIcs Volume Portal

Wachter, Björn

Explaining Data Type Reduction in the Shape Analysis Framework

pdf-format:
06000.WachterBjoern.ExtAbstract.701.pdf (0.2 MB)

Abstract

Automatic formal verification of systems composed of a large or even unbounded
number of components is difficult as the state space of these systems is
prohibitively large. Abstraction techniques automatically construct finite
approximations of infinite-state systems from which safe information about
the original system can be inferred. We study two abstraction techniques
shape analysis, a technique from program analysis, and data type reduction,
originating from model checking. Until recently we did not properly understand
how shape analysis and data type reduction relate. In this talk, we shed light
on this relation in a comprehensive way. This is a step towards a more
unified view of abstraction employed in the static analysis and model checking
community.

BibTeX - Entry

@InProceedings{wachter:OASIcs:2006:701,
  author =	{Bj{\"o}rn Wachter},
  title =	{{Explaining Data Type Reduction in the Shape Analysis Framework}},
  booktitle =	{Workshop on Trustworthy Software},
  series =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-02-6},
  ISSN =	{2190-6807},
  year =	{2006},
  volume =	{3},
  editor =	{Serge Autexier and Stephan Merz and Leon van der Torre and Reinhard Wilhelm and Pierre Wolper},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2006/701},
  URN =		{urn:nbn:de:0030-drops-7016},
  doi =		{10.4230/OASIcs.TrustworthySW.2006.701},
  annote =	{Keywords: Canonical abstraction, data type reduction, model checking, parameterized system, infinite-state}
}

Keywords: Canonical abstraction, data type reduction, model checking, parameterized system, infinite-state
Collection: Workshop on Trustworthy Software
Issue Date: 2006
Date of publication: 26.09.2006

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