Finding loop invariants using tree grammars

Abstract

This thesis applies a method for inductive theorem proving based on tree grammars developed by Eberhard and Hetzl to the generation of loop invariants. We consider the verification of simple loops, which do not contain nested loops, and invariants with a single universal quantifier. The verification of this class of programs is reduced to the existing method for inductive proofs, giving an automated method for finding loop invariants. Chapter 1 contains a new exposition of the existing work on tree grammars, culminating in an efficient algorithm to find a minimal grammar covering a given language. Such a minimal grammar consists of productions in a normal form---these normal forms are described using a logic of term algebras. We also investigate the relation to anti-unification. In chapters 2 and 3 we summarize the existing work on proofs and their grammars. The extraction of Herbrand sequents from cut-free proofs is generalized to proofs with universally quantified cuts: there we can extract a totally rigid tree grammar; for proofs with a single induction, we obtain sip grammars. Inverting this extraction allows us introduce cuts, or induction, respectively. The case of inductive proofs and their sip grammars is slightly generalized to allow for the reduction of loop verification problems. In chapters 4 and 5 the verification of loops without nested loops is reduced to the inductive case. This reduction induces a class of grammars; we give an algorithm for efficiently finding a minimal grammar in this class that covers a given language.