An interpretation oriented theorem prover over integers
James C. King, Robert W. Floyd
STOC 1970
A study of several of the proof of correctness methods is presented. In particular, the form of induction used is explored in detail. A relational semantic model for programming languages is introduced and its relation to predicate transformers is explored. A rather elementary viewpoint is taken in order to expose, as simply as possible, the basic differences of the methods and the underlying principles involved. These results were obtained by attempting to thoroughly understand the “subgoal induction” method. Copyright © 1980 by The Institute of Electrical and Electronics Engineers, Inc.
James C. King, Robert W. Floyd
STOC 1970
James C. King
International Conference on Reliable Software 1975
Sidney L. Hantler, James C. King
ACM Computing Surveys (CSUR)
James C. King
IEEE TC