Automatic Assume/Guarantee Reasoning for Heap-Manipulating Programs
Greta Yorsh, Alexey Skidanov, Thomas Reps, and Mooly Sagiv
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.
(Click here to access the paper:
PostScript,
PDF.)