Campus Event Calendar
Event Entry
What and Who
Shape Analysis of Sets
Jan Reineke
PhD Application Talk
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
Monday, 4 July 2005
14:00
-- Not specified --
46.1 - MPII
024
Saarbrücken
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.
Contact
Kerstin Meyer-Ross
9325-226
--email hidden
passcode not visible
logged in users only
Christine Kiesel, 06/30/2005 18:28
Christine Kiesel, 06/30/2005 18:17 -- Created document.
Christine Kiesel, 06/30/2005 18:17 -- Created document.