**Abstract:** We present different approaches of using a special purpose computer algebra system and theorem provers in software verification. To this end, we first develop a purely algebraic while-program for computing a vertex coloring of an undirected (loop-free) graph. For showing its correctness, we then combine the well-known assertion-based verification method with relation-algebraic calculations. Based on this, we show how automatically to test loop-invariants by means of the RelView tool and also compare the usage of three different theorem provers in respect to the verification of the proof obligations: the automated theorem prover Prover9 and the two proof assistants Coq and Isabelle/HOL. As a result, we illustrate that algebraic abstraction yields verification tasks that can easily be verified with off-the-shelf theorem provers, but also reveal some shortcomings and difficulties with theorem provers that are nowadays available.

**Paper:** pdf

This webpage contains the input files for Prover9, Coq and Isabelle/HOL.

**Verification of Proof Obligations using Prover9**

Prover9 is a resolution- and paramodulation-based automated theorem prover for first-order and equational logic. It is, however, very limited with regard to typing. Therefore, we decided to restrict our experiments to homogenous relation algebra. We use the symbols `^`

, `'`

, `\/`

, `/\`

and `*`

for transposition, complement, union, intersection and composition, respectively.

For each result we want to prove automatically, we create one input file.

**Verification of Proof Obligations using Coq**

Since the functionality of Coq is based on the predicative calculus of inductive constructions (pCIC) each object has a type. Thus, heterogeneous relation algebra can be modeled, and it has already been done within a relation-algebra library. This library does not only include a model for heterogeneous relation algebra but also for a large number of other algebraic structures.

The symbols ```

, `!`

, `+`

, `^`

, and `*`

are used for transposition, complement, union, intersection, and composition, respectively.

Our proofs can be downloaded here.

**Verification of Proof Obligations using Isabelle/HOL**

Similar to Coq, libraries can be included in Isabelle/HOL. As in the case of Coq, (homogeneous) relation algebra has already be formalised in Isabelle/HOL and can be downloaded here (this libary builds on this one here)

Our proofs can be downloaded here.

**Contact:** Peter Höfner: peter.hoefner <at> nicta.com.au