Issue No. 01 - March (1975 vol. 1)
Steven M. German , Xerox Research Center, Palo Alto, Calif. 94304; Center for Research in Computing Technology, Harvard University, Cambridge, Mass
Ben Wegbreit , Xerox Research Center, Palo Alto, Calif. 94304
Most current methods for mechanical program verification require a complete inductive assertion on each loop. As this is tedious and error prone, producing a program with complete, correct assertions is moderately difficult. This paper 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. We present Vista as a step toward practical program verifiers.
Junctions, Synthesizers, Prototypes, Arrays, Data mining, Testing, Generators, weak interpretations, Completing inductive assertions, inductive assertions, loop invariants, loop predicates, program verification, synthesis of inductive assertions, theorem proving
S. M. German and B. Wegbreit, "A synthesizer of inductive assertions," in IEEE Transactions on Software Engineering, vol. 1, no. , pp. 68-75, 1975.