The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.01 - March (1975 vol.1)
pp: 68-75
Ben Wegbreit , Xerox Research Center, Palo Alto, Calif. 94304
ABSTRACT
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.
INDEX TERMS
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
CITATION
Ben Wegbreit, "A synthesizer of inductive assertions", IEEE Transactions on Software Engineering, vol.1, no. 1, pp. 68-75, March 1975, doi:10.1109/TSE.1975.6312821
17 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool