Campus Event Calendar
Event Entry
What and Who
Symbolic Shape Analysis
Thomas Wies
Ringvorlesung
AG 1, AG 2, AG 3, AG 4, AG 5
AG Audience
Note: We use this to send email in the morning.
Date, Time and Location
Thursday, 8 December 2005
13:00
-- Not specified --
45 - FR 6.2 (E1 3)
016
Saarbrücken
Abstract
Software model-checkers such as SLAM and BLAST are tools that automatically verify software. The success of these tools lies in the fact that they use symbolic methods, meaning that the program is represented in terms of logical formulas and the analysis of the program amounts to deductive reasoning over these formulas. Currently the applicability of software model-checkers is limited if a program manipulates heap-allocated data structures. These limitations become apparent, when the correct execution of the program depends on a data structure's shape. For instance, the termination of a program that traverses a recursive data structure might depend on the fact that this data structure forms a directed acyclic graph. Shape analysis is a technique that deals with the verification of such data structure properties. We introduce symbolic shape analysis. Symbolic shape analysis extends the capabilities of software-model checkers for programs with dynamic memory allocation.
Contact
--email hidden
passcode not visible
logged in users only
Veronika Weinand, 12/05/2005 12:59
Veronika Weinand, 10/19/2005 13:11
Veronika Weinand, 10/19/2005 13:08 -- Created document.
Veronika Weinand, 10/19/2005 13:11
Veronika Weinand, 10/19/2005 13:08 -- Created document.