Heap assertions on demand

  • Andreas Podelski | University of Freiburg, Germany

Systems code is prone to termination errors. Inferring preconditions excluding such errors is both tedious and hard.
This is true in particular for heap manipulating functions.
Both, a precondition and the invariants used to prove termination must express what heap locations or regions can be aliased, inter-reachable, separated or shared. Shape analysis to compute such heap assertions is notoriously expensive. Our new termination analysis with precondition inference calls shape analysis on demand. The computed heap assertion is either a valid invariant that must be made explicit during the termination proof, or it is a precondition that must be added in order to ensure correctness. This is joint work with Andrey Rybalchenko and Thomas Wies.

Speaker Details

Andreas Podelski’s scientific life includes intervals spent at Brown University, Paris 7, Berkely, DEC PRL, and MPI Saarbrücken. Presently, he teaches at the University of Freiburg, Germany. His research interests are program analysis and verification.

    • Portrait of Jeff Running

      Jeff Running

Watch Next