Symbolic Shape Analysis

Wies, Thomas

Local TagsRelease HistoryDetailsSummary

Symbolic Shape Analysis

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

Item is Released

show all hide all

Basic

show hide

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

Genre: Thesis

Files

show Files

Locators

show

Creators

show

hide

Creators:
Wies, Thomas¹, Author

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

Content

show

hide

Free keywords: -

Abstract: 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.

Details

show

hide

Language(s): eng - English

Dates: Accepted: 2004Date issued: 2004

Publication Status: Issued

Pages: -

Publishing info: Saarbrücken : Universität des Saarlandes

Table of Contents: -

Rev. Type: -

Identifiers: eDoc: 231273
BibTex Citekey: Wies2004
Other: Local-ID: C1256104005ECAFC-952441E206ED7310C1256F870035AF04-Wies2004

Degree: Diploma

Event

show

Legal Case

show

Project information

show

Source

show