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

Reineke, Jan

Shape Analysis of Sets

pdf-format:
06000.ReinekeJan.Other.698.pdf (1 MB) 06000.ReinekeJan.Paper.698.pdf (0.4 MB)

Abstract

Shape Analysis is concerned with determining "shape invariants", i.e. structural properties of the heap, for programs that manipulate pointers and heap-allocated storage. Recently, very precise shape analysis algorithms have been developed that are able to prove the partial correctness of heap-manipulating programs. We explore the use of shape analysis to analyze abstract data types (ADTs). The ADT Set shall serve as an example, as it is widely used and can be found in most of the major data type libraries, like STL, the Java API, or LEDA. We formalize our notion of the ADT Set by algebraic specification. Two prototypical C set implementations are presented, one based on lists, the other on trees. We instantiate a parametric shape analysis framework to generate analyses that are able to prove the compliance of the two implementations to their specification.

BibTeX - Entry

@InProceedings{reineke:OASIcs:2006:698,
  author =	{Jan Reineke},
  title =	{{Shape Analysis of Sets}},
  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/698},
  URN =		{urn:nbn:de:0030-drops-6980},
  doi =		{10.4230/OASIcs.TrustworthySW.2006.698},
  annote =	{Keywords: Shape analysis, adt, algebraic specification, invariants, verification, set implementations, imperative programs}
}

Keywords: Shape analysis, adt, algebraic specification, invariants, verification, set implementations, imperative programs
Collection: Workshop on Trustworthy Software
Issue Date: 2006
Date of publication: 26.09.2006

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