Programme of HAV at ETAPS 2007

(Heap Analysis and Verification)

Sunday, March 25, room: CP2-104

09:00 - 10:30 SESSION 1

Footprint Analysis: A Shape Analysis that Discovers Preconditions (Invited Lecture)
Hongseok Yang
Proof Systems for Inductive Reasoning in the Logic of Bunched Implications
James Brotherston

10:30 - 11:00 Coffee Break

11:00 - 12:30 SESSION 2

A Logic of Reachable Patterns (Invited Lecture)
Greta Yorsh
Verifying Complex Properties using Symbolic Shape Analysis
Thomas Wies, Viktor Kuncak, Karen Zee, Martin Rinard and Andreas Podelski

12:30 - 14:00 Lunch

14:00 - 16:00 SESSION 3

Alias Control with Universe Types (Invited Lecture)
Peter Müller
Inferring Local (Non-)Aliasing and Strings for Memory Safety
Yannick Moy and Claude Marché
Reasoning about Sequences of Memory States
Brochenin Rémi, Demri Stéphane and Lozes Étienne

16:00 - 16:30 Coffee Break

16:30 - 18:00 SESSION 4

Liveness of Heap Data for Functional Programs
Amey Karkare, Uday Khedker and Amitabha Sanyal
Separation Analysis for Deductive Verification
Thierry Hubert and Claude Marché
Verifying Concurrent List-Manipulating Programs by LTL Model Checking
Stefan Rieger, Thomas Noll and Joost-Pieter Katoen
Towards Regional Logic (Invited Lecture)
David Naumann


Joint Workshops Pre-Conference Dinner (tickets needed)
Dinner at Bom Jesus, Braga
Shuttle departure from University Campus, Gualtar

Further ETAPS 2007 Programme Information:

ETAPS 2007 | Top | HTML 4.01 | Last Update: 2007-03-13