Heap Analysis and Verification

HAV 2007

 

March 25, 2007, Braga, Portugal

a satellite workshop of ETAPS 2007

 

start

end

title

speaker / authors

9:00

10:00

Invited lecture: Footprint Analysis: A Shape Analysis that Discovers Preconditions

Hongseok Yang

10:00

10:30

Proof Systems for Inductive Reasoning in the Logic of Bunched Implications

James Brotherston

10:30

11:00

coffee break

11:00

12:00

Invited lecture: A Logic of Reachable Patterns

Greta Yorsh

12:00

12:30

Verifying Complex Properties using Symbolic Shape Analysis

Thomas Wies, Viktor Kuncak, Karen Zee, Martin Rinard and Andreas Podelski

12:30

2:00

lunch

2:00

3:00

Invited lecture: Alias Control with Universe Types

Peter Müller

3:00

3:30

Inferring Local (Non-)Aliasing and Strings for Memory Safety

Yannick Moy and Claude Marché

3:30

4:00

Reasoning about Sequences of Memory States

Brochenin Rémi, Demri Stéphane and Lozes Étienne

4:00

4:30

coffee break

4:30

4:50

Liveness of Heap Data for Functional Programs

Amey Karkare, Uday Khedker and Amitabha Sanyal

4:50

5:10

Separation Analysis for Deductive Verification

Thierry Hubert and Claude Marché

5:10

5:30

Verifying Concurrent List-Manipulating Programs by LTL Model Checking

Stefan Rieger, Thomas Noll and Joost-Pieter Katoen

5:30

6:30

Invited lecture: Automata-Based Techniques for the Verification of Programs with Linked Data Structures

Ahmed Bouajjani