Automatic Assume/Guarantee Reasoning for Heap-Manipulating Programs
Greta Yorsh, Alexey Skidanov, Thomas Reps, Mooly Sagiv · Electronic Notes in Theoretical Computer Science · 2005
Assume/Guarantee (A/G) reasoning for heap-manipulating programs is challenging because the heap can be mutated in an arbitrary way by procedure calls. Moreover, specifying the potential side-effects of a procedure is non-trivial. We report on an on-going effort to reduce the burden of A/G reasoning for heap-manipulating programs by automatically generating post-conditions and estimating side-effects of non-recursive procedures. Our method is sound. It combines the use of theorem provers and abstract-interpretation algorithms.