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