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.
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
Last update: Apr. 01, 2015