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 complex proofs.

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.
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 proof database.
©2008. Peter Höfner