Automated Verification of Refinement Laws
P. Höfner, G. Struth, G. Sutcliffe
(to appear), 2008.
Demonic refinement algebras are variants of Kleene algebras. Introduced
by von Wright as a light-weight variant of the refinement calculus, their
intended semantics are positively disjunctive predicate transformers, and their
calculus is entirely within first-order equational logic. So, for the first
time, off-the-shelf automated theorem proving (ATP) becomes available for
refinement proofs. We used ATP to verify a toolkit of basic refinement laws.
Based on this toolkit, we then verified two classical complex refinement laws
for action systems by ATP: a data refinement law and Back's atomicity refinement
law. We also present a refinement law for infinite loops that has been
discovered through automated analysis. Our proof experiments not only
demonstrate that refinement can effectively be automated, they also compare
eleven different ATP systems and suggest that program verification with variants
of Kleene algebras yields interesting theorem proving benchmarks. Finally, we
apply hypothesis learning techniques that seem indispensable for automating more
1 Please note that our database is undergoing a major revision. Therefore the files may slighty differ from the version described in the
paper. We are sorry for
any inconvinience we cause.
The input files for the evaluation of different theorem provers can be downloaded here.
In our input files are hard-coded paths describbing the location of the file containing the axioms.
When using the files it might be necessary to modify this path.
- We used Prover9 to show those lemmas which we could not show immedeately.
For that we used some sort of hypothesis learning (see the paper for details).
The input/output files for Prover9 can be found in our database
in the category Demonic Refinement Algebra.1
We have done more proof experiments, including idempotent
semirings, Kleene algebras, omega algebras and demonic refinement
algebras. The files concerning these experiments can be found in a