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

18:45 SOCIAL EVENT

Joint Workshops Pre-Conference Dinner (tickets needed)

Dinner at Bom Jesus, Braga

Shuttle departure from University Campus, Gualtar

Further ETAPS 2007 Programme Information:

• Programme Overview, Social Programme
• Main Conferences: Complete Programme, CC, ESOP, FASE, FOSSACS, TACAS
• Workshops: ACCAT, Bytecode, COCV, FESCA, FinCo, GT-VMT, HFL, LDTA, MBT, MOMPES, OpenCert, QAPL, SC, SLA++P, TERMGRAPH, WITS
• Tutorials: Stratego/XT, SoftwGen, Mobius