Automated Verification of Relational While-Programs

Abstract: Software verification is essential for safety-critical systems. In this paper, we illustrate that some verification tasks can be done fully automatically. We show how to automatically verify imperative programs for relation-based discrete structures by combining relation algebra and the well-known assertion-based verification method with automated theorem proving. We present two examples in detail: a relational program for determining the reflexive-transitive closure and a topological sorting algorithm. We also treat the automatic verification of the equivalence of common-logical and relation-algebraic specifications.

Paper: pdf

The first algorithm we are going to verify with the help of Prover9 is an algorithm for computing the reflexive-transitive closure for a given relation.

To verify this algorithm we establish two invariants.

Invariants

Prover9 can verify partial correctness of this algorithm, using the following input files (for more details, we refer to the paper). Next to the input files, we also list running times.

Establishment
	0s	input
Maintenance
	1s	input
	0s	input
Post-Condition
	0s	input

The first law of maintenance could not be proven with our standard input file.We had to add three auxiliary facts about the Kleene star.However, all these facts could be proven fully automatically without any interaction.

Auxiliary Facts
	73s	input
	248s	input
	184s	input

So far we have established partial correctness of the algorithm.However, for this algorithm we can even show total correctness with the help of Prover9.For this proof the following properties are sufficient.

Termination
	0s	input
	1s	input
1	0s	input
	0s	input

¹In this example Prover9 finds a proof, but outputs "SEARCH FAILED"followed by "Exiting with 1 proof" (or some other number).A close inspection of the proof logs showed that such situations occur in case negative clauses are included in the goals.Then the output is misleading, since in such cases Prover9 did find a proof, but thought it had to keep searching

The second algorithm we verify is an algorithm for topological sorting.

To verify this algorithm we establish two invariants.

Invariants

As abbreviation we use

Prover9 can verify partial correctness of this algorithm, using the following input files (for more details, we refer to the paper).

Establishment
	0s	input
	0s	input
	0s	input
	0s	input
	0s	input
	0s	input
	0s	input
	0s	input
Maintenance
	0s	input
	22s	input
	3s	input
	1s	input
	0s	input
	43s	input
	24s	input
	0s	input
Post-Condition
	0s	input

The establishment of the invariants can be done without splitting:

1s

input

So far we have established partial correctness of the algorithm.However, for this algorithm we can again total correctness; it is similar to the above.

Termination
	0s	input
	0s	input

Above we have automatically proven total correctness for two relational while programs. One reason why we could use automated theorem provers is that we are able to write program specifications as relational expressions. However, often specifications and program properties are not given in a relation-algebraic manner;but in predicate-logic. Luckily, it is easy to show equivalences between logical and relation-algebraic specifications.

	0s	input
	0s	input
	0s	input
	1s	input
	0s	input
	2.5s	input

Note: The relation-algebraic expression inside the tables follow the paper and use the same notation; the input files, however, often make use of Prover9's feature of "automated quantifying". This feature only works for variables named u,v,w,x,y and z. That is why the input files sometimes use different variable names.

Contact: Peter Höfner: peter <at> hoefner-online.de