Heap Analysis and Verification HAV 2008 July 14, 2008, Princeton, New Jersey a workshop affiliated with CAV’08
Speakers Alexey Gotsman (University of Cambridge) Sumit Gulwani (Microsoft Research) Roman Manevich (Tel Aviv University) Bill McCloskey (UC Berkeley) Ken McMillan (Cadence Berkeley Labs) Shaz Qadeer (Microsoft Research) Thomas Wies (University of Freiburg) Hongseok Yang (Queen Mary, University of London) Organizers Josh Berdine (Microsoft Research) Mooly Sagiv (Tel Aviv University) Eran Yahav (IBM Research)		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. 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

Supported by