AUTOMATED THEOREM PROVING
29
"certifying" the program correct; and because the verification
condition statements are often long and complex, although the
proofs are not deep
in
comparison with a typical theorem of
interest to mathematicians.
A system that began quite early, in 1972, is the Stanford PAS-
CAL verifier. The effort began with Shigeru Igarashi, Ralph London
and David Luckham with later development by Nori Suzuki and
others (see [Pol]). Its significance for us is that its development
led to some notable work on decision procedures by Oppen and
Nelson [NOl], work we have alluded to previously. The primary
techniques used are rewrite rules and decision procedures. The
key to good theorem proving of verification conditions is
simplification of expressions. There is disagreement as to whether
rewrite rules or decision procedures are the preferred technology.
for simplification, with Oppen and Nelson on the apparent minority
side favoring decision procedures.
The GYPSY verification project directed by Donald Good
[Go2],[GC 1] at the U. of Texas has demonstrated itself as a major
system by verifying a particular security property holds
throughout a rather large (about 4000 lines) and complex pro-
gram. The project, begun about 1974, uses a version of the Bled-
soe theorem prover for its inference-making. Another verifier of
importance is the AFFIRM system[GMl] developed by Dave Musser
and Susan Gerhart at lSI (Santa Monica, California) beginning
about 1976. Neither GYPSY nor AFF1RM need work directly with
executable code but can verify algorithms at a somewhat more
abstract level. AFFIRM is notable for its capability with abstract
data types, which are data structures and associated operators
that are governed by axioms. AFFIRM also uses a rewrite rule
sys-
tem, and the project has led to contributions to our understand-
ing of such systems (see Musser [Mu2]). We mention one other
Previous Page Next Page