Completion Based Inductive Theorem Proving : A Case Study in Verifying Sorting Algorithms

Abstract

The focus of this paper lies on practical aspects of completion based inductive theorem proving in equational theories. As domain of interest we concentrate on the mechanically supported verification of a couple of sorting algorithms. The experiments have been performed with UNICOM, an inductive theorem prover based on refined unfailing completion techniques. We summarize these experiments, point out important technical and conceptual aspects and illustrate them by numerous examples. In particular we discuss and exemplify the kind of intelligent proof engineering required for succeeding in non-trivial verification problems.