Heap assertions on demand

Опубликовано 6 сентября 2016, 16:48

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.