Heap Analysis and Verification

HAV 2007

March 25, 2007, Braga, Portugal

a satellite workshop of ETAPS 2007

program

Program Commitee

• Josh Berdine (Microsoft Research, Cambridge, co-chair)
• Ahmed Bouajjani (University of Paris 7)
• Cristiano Calcagno (Imperial College London)
• Greg Morrisett (Harvard University)
• Viktor Kuncak (EPFL)
• Shuvendu Lahiri (Microsoft Research. Redmond)
• Arnd Poetzsch-Heffter (TU Kaiserslautern)
• Radu Rugina (Cornell University)
• Mooly Sagiv (Tel-Aviv University, Israel, co-chair)
• Eran Yahav (IBM Watson)

Important Dates

Paper submission	Jan 5, 2007 Jan 10, 2007
Notification of acceptance	Jan 26, 2007 Feb 5, 2007
Final copy due	Feb 9, 2007 Feb 16, 2007
Early registration	Feb 12, 2007
Workshop	Mar 25, 2007

Invited Speakers

• Ahmed Bouajjani (University of Paris 7)
• Peter Müller (ETH Zürich)
• Hongseok Yang (Queen Mary, University of London)
• Greta Yorsh (Tel-Aviv University)

Call for Papers

Organizers

• Josh Berdine
• Mooly Sagiv

Aim and Scope

Accurate and efficient expression, discovery, and verification of the structure of program heap memory is an active research area.  Many problems remain open, and therefore many programs remain unverified. We are seeing advances however: Among these are exciting new techniques for analysis and verification of concurrently accessed heap memory, new techniques for interprocedural and modular analysis and verification, and great strides increasing the range of practically applicable analysis and verification techniques.

The aim of this workshop is to bring together researchers to exchange and develop new ideas in all aspects of formal analysis and verification for heaps.  Submissions are invited from across the full spectrum of basic theoretical work through to applied practical work.

Topics of Interest

Topics of particular interest (non-exclusively) include:

• shape analysis
• abstract interpretation, program analysis, and model checking for heap programs
• logics and type systems for expressing or verifying heap properties
• automation and mechanization of such logics
• graph and other models of the heap
• comparisons of existing techniques and tools
• test cases and experimental results

Proceedings

A formal proceedings will not be published.  A CD with an informal proceedings was distributed at the conference.

Paper Submission

Submission is closed.