Automated verification of refinement laws

Peter Höfner, Georg Struth, Geoffrey Sutcliffe

Research output: Contribution to journalArticle

8 Citations (Scopus)

Abstract

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.

Original languageEnglish (US)
Pages (from-to)35-62
Number of pages28
JournalAnnals of Mathematics and Artificial Intelligence
Volume55
Issue number1-2
DOIs
StatePublished - Oct 2009

Fingerprint

Theorem proving
Refinement
Automated Theorem Proving
Algebra
Kleene Algebra
Calculus
Equational Logic
Semantics
Atomicity
Program Verification
Theorem Proving
Transformer
First-order Logic
Predicate
Benchmark
Verify
Experiments

Keywords

  • Action systems
  • Automated deduction
  • Kleene algebras
  • Refinement calculus

ASJC Scopus subject areas

  • Artificial Intelligence
  • Applied Mathematics

Cite this

Automated verification of refinement laws. / Höfner, Peter; Struth, Georg; Sutcliffe, Geoffrey.

In: Annals of Mathematics and Artificial Intelligence, Vol. 55, No. 1-2, 10.2009, p. 35-62.

Research output: Contribution to journalArticle

Höfner, Peter ; Struth, Georg ; Sutcliffe, Geoffrey. / Automated verification of refinement laws. In: Annals of Mathematics and Artificial Intelligence. 2009 ; Vol. 55, No. 1-2. pp. 35-62.
@article{b246f044c03f470682c0a45c6df7f1a8,
title = "Automated verification of refinement laws",
abstract = "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.",
keywords = "Action systems, Automated deduction, Kleene algebras, Refinement calculus",
author = "Peter H{\"o}fner and Georg Struth and Geoffrey Sutcliffe",
year = "2009",
month = "10",
doi = "10.1007/s10472-009-9151-8",
language = "English (US)",
volume = "55",
pages = "35--62",
journal = "Annals of Mathematics and Artificial Intelligence",
issn = "1012-2443",
publisher = "Springer Netherlands",
number = "1-2",

}

TY - JOUR

T1 - Automated verification of refinement laws

AU - Höfner, Peter

AU - Struth, Georg

AU - Sutcliffe, Geoffrey

PY - 2009/10

Y1 - 2009/10

N2 - 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.

AB - 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.

KW - Action systems

KW - Automated deduction

KW - Kleene algebras

KW - Refinement calculus

UR - http://www.scopus.com/inward/record.url?scp=70350381800&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=70350381800&partnerID=8YFLogxK

U2 - 10.1007/s10472-009-9151-8

DO - 10.1007/s10472-009-9151-8

M3 - Article

AN - SCOPUS:70350381800

VL - 55

SP - 35

EP - 62

JO - Annals of Mathematics and Artificial Intelligence

JF - Annals of Mathematics and Artificial Intelligence

SN - 1012-2443

IS - 1-2

ER -