Decision Procedure for Program Verification
Original Publication Date: 1978-Aug-01
Included in the Prior Art Database: 2005-Feb-21
A primitive programming structure is formed in which to define any bounded function. Means RT are given for transforming such a primitive program P into a logical (hardware) realization L(P). It is proven that L(P) performs the same function as P. Program P is said to be "verified" if it is proven functionally equivalent to another program Q known to perform the correct function. The verification procedure here is to transform P and Q into Logic Realizations L(P) and L(Q) and then to apply the hardware verification algorithm VERIFY to ascertain equivalence/inequivalence [1,2]. If they are not equivalent, a counter example is constructed. Theorem: P,Q are equivalent if and only if L(P), L(Q) are. The run time for RT is a linear and for VERIFY, an exponential function of P's, Q's complexity.