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 |