AHA 2007
International symposium on
Automatic Heap Analysis
 July 2nd 2007  Berlin, Germany
satellite event of CAV 2007
Aim and Scope

One of the frontiers of formal software verification is the analysis of dynamically allocated and recursive data structures.  This symposium aims at bringing together leaders in the field of automatic heap analysis as well as researchers interested in the field. We have invited 10 speakers representing different communities (including predicate abstraction, 3-valued logic, separation logic, graph transformation systems, software model checking, etc.).



Speakers

Ahmed Bouajjani,
University of Paris 7, France 

Cristiano Calcagno
Imperial College, London, UK

Tom Henzinger,
EPFL Lausanne, Switzerland   
   
Shuvendu Lahiri,
Microsoft Research, Redmond, USA
 
Ken McMillan,
Cadence Berkeley Labs
   
Amir Pnueli,
New York University, USA
 
Andreas Podelski,
University of Freiburg, Germany

Arend Rensink,
University of Twente, The Netherlands

Radu Rugina,
Cornell University, USA
      
Mooly Sagiv,
Tel-Aviv University, Israel    


Preliminary Program
9:30-10:00     Symbolic Shape Analysis [Slides]
                        Andreas Podelski
10:00- 10:30  Shape Analysis with tracked cells [Slides]
                        Radu Rugina

10:30-11:00 Coffee Break

11:00-11:30  Automata-based techniques for shape analysis [Slides]
                       Ahmed Bouajjani
11:30-12:00  Path Invariants [Slides]
                        Tom Henzinger
12:00-12:30   Abstraction in Graph Transformation [Slides]
                        Arend Rensink

12:30-14:00 Lunch

14:00-14:30  Shape Analysis with Precise Abstraction [Slides]
                       Amir Pnueli
14:30-15:00  Partially Disjunctive Shape Analysis [Slides]
                       Mooly Sagiv
15:00-15:30 Can logic tame systems programs? [Slides]
                      Cristiano Calcagno

15:30-16:00 Coffee Break

16:00-16:30 Constructing quantified invariants using interpolants [Slides]
                      Ken McMillan
16:30-17:00 HAVOC: Heap Aware Verification Of C programs [Slides]
                      Shuvendu Lahiri
Organizers

Byron Cook,
Microsoft Research Cambridge, UK

Dino Distefano,
Queen Mary University of London, UK