USING TERM REWRITING TO VERIFY SOFTWARE

This paper describes a uniform approach to the automation of verificat ion tasks associated with while statements, representation functions f or abstract data types, generic program units, and abstract base class es. Program units are annotated with equations containing symbols defi ned by algebraic axioms. An operation's axioms are developed by using strategies that guarantee crucial properties such as convergence and s ufficient completeness. Sets of axioms are developed by stepwise exten sions that preserve these properties. Verifications are performed with the aid of a program that incorporates term rewriting, structural ind uction, and heuristics based on ideas used in the Boyer-Moore prover. The program provides valuable mechanical assistance: managing inductiv e arguments and providing hints for necessary lemmas, without which fo rmal proofs would be impossible. The successes and limitations of our approaches are illustrated with examples from each domain.