[ The Types Forum (announcements only), 
     http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]

Call for Participation

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.).

- Ahmed Bouajjanni (University of Paris 7, France)
  "Automata-based techniques for shape analysis"

- Cristiano Calcagno (Imperial College, London, UK)
  "Can logic tame systems programs?"

- Tom Henzinger (EPFL Lausanne, Switzerland)
  "Lazy Abstraction Refinement"

- Shuvendu Lahiri (Microsoft Research, Redmond, USA)
  "HAVOC: Heap Aware Verification Of C programs"

- Ken McMillan (Cadence Berkeley Labs)
  "Constructing quantified invariants using interpolants"

- Amir Pnueli (New York University, USA)
  "Shape Analysis with Precise Abstraction"

- Andreas Podelski (University of Freiburg, Germany)
  "Symbolic Shape Analysis"

- Arend Rensink (University of Twente, The Netherlands)
  "Abstraction in Graph Transformation"

- Radu Rugina (Cornell University, USA)
  "Shape Analysis with tracked cells"

- Mooly Sagiv (Tel-Aviv University, Israel)
  "Partially Disjunctive Shape Analysis"

Byron Cook,
Microsoft Research Cambridge, UK

Dino Distefano,
Queen Mary University of London, UK

Reply via email to