Symbolic Shape Analysis

Wies, Thomas

Lokale TagsFreigabegeschichteDetailsÜbersicht

Symbolic Shape Analysis

Wies, T. (2004). Symbolic Shape Analysis. Diploma Thesis, Universität des Saarlandes, Saarbrücken.

Item is Freigegeben

einblenden: alle ausblenden: alle

Basisdaten

einblenden: ausblenden:

Datensatz-Permalink: https://hdl.handle.net/11858/00-001M-0000-000F-256D-1 Versions-Permalink: https://hdl.handle.net/11858/00-001M-0000-0023-F106-7

Genre: Hochschulschrift

ausblenden:

Urheber:
Wies, Thomas¹, Autor

Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045

Inhalt

einblenden:

ausblenden:

Schlagwörter: -

Zusammenfassung: Shape analysis deals with the synthesis of invariants for programs manipulating heap-allocated data structures. Explicit shape analysis algorithms do not scale very well. This work proposes a framework for symbolic shape analysis that addresses this problem. Our contribution is a framework that allows to abstract programs with heap-allocated data symbolically by Boolean programs. For this purpose, we combine abstraction techniques from shape analysis with ideas from predicate abstraction. Our framework is parameterized by a set of abstraction predicates. We propose a class of predicates that can be used to analyze reachability properties for linked data structures. This class may potentially be used for automated abstraction refinement.