A synthesizer of inductive assertions

Abstract

Describes a prototype system Vista which provides assistance in synthesizing correct inductive assertions. Given only the source program, it is able to generate a useful class of assertions automatically. For a larger class, it is able to extend partial inductive assertions supplied by the programmer to form complete assertions from which it proves program correctness. Its synthesis methods include: symbolic evaluation in a weak interpretation, combining output assertions with loop exit information to obtain trail loop assertions, and extracting information from proofs which fail in order to determine how assertions should be strengthened.