The Use of Rippling to Automate Event-B Invariant Preservation Proofs

Yuhui Lin; Alan Bundy; Gudmund Grov

doi:10.1007/978-3-642-28891-3_23

The Use of Rippling to Automate Event-B Invariant Preservation Proofs

Yuhui Lin, Alan Bundy, Gudmund Grov

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract / Description of output

Proof automation is a common bottleneck for industrial adoption of formal methods. In Event-B, a significant proportion of proof obligations which require human interaction fall into a family called invariant preservation . In this paper we show that a rewriting technique called rippling can increase the automation of proofs in this family, and extend this technique by combining two existing approaches.

Original language	English
Title of host publication	NASA Formal Methods
Subtitle of host publication	4th International Symposium, NFM 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings
Editors	Alwyn Goodloe, Suzette Person
Publisher	Springer
Pages	231-236
Number of pages	6
ISBN (Electronic)	978-3-642-28891-3
ISBN (Print)	978-3-642-28890-6
DOIs	https://doi.org/10.1007/978-3-642-28891-3_23
Publication status	Published - 2012

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer Berlin / Heidelberg
Volume	7226
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Keywords / Materials (for Non-textual outputs)

Event-B
automated reasoning
rippling
lemma conjecture

Access to Document

10.1007/978-3-642-28891-3_23

Yuhui NFM12Submitted manuscript, 95 KB

https://link.springer.com/chapter/10.1007%2F978-3-642-28891-3_23

A14FM : using A1 to aid automation of proof search in formal methods
Bundy, A., Bundy, A., Grov, G., Ireland, A. & Jones, C. B.
EPSRC
1/04/10 → 31/03/14
Project: Research

Cite this

@inproceedings{e1561ae7a1c949dd969ad0e92394aaa2,

title = "The Use of Rippling to Automate Event-B Invariant Preservation Proofs",

abstract = "Proof automation is a common bottleneck for industrial adoption of formal methods. In Event-B, a significant proportion of proof obligations which require human interaction fall into a family called invariant preservation . In this paper we show that a rewriting technique called rippling can increase the automation of proofs in this family, and extend this technique by combining two existing approaches.",

keywords = "Event-B, automated reasoning, rippling, lemma conjecture",

author = "Yuhui Lin and Alan Bundy and Gudmund Grov",

year = "2012",

doi = "10.1007/978-3-642-28891-3_23",

language = "English",

isbn = "978-3-642-28890-6",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "231--236",

editor = "Alwyn Goodloe and Suzette Person",

booktitle = "NASA Formal Methods",

}

The Use of Rippling to Automate Event-B Invariant Preservation Proofs. / Lin, Yuhui; Bundy, Alan; Grov, Gudmund.
NASA Formal Methods: 4th International Symposium, NFM 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings. ed. / Alwyn Goodloe; Suzette Person. Springer, 2012. p. 231-236 (Lecture Notes in Computer Science; Vol. 7226).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

TY - GEN

T1 - The Use of Rippling to Automate Event-B Invariant Preservation Proofs

AU - Lin, Yuhui

AU - Bundy, Alan

AU - Grov, Gudmund

PY - 2012

Y1 - 2012

N2 - Proof automation is a common bottleneck for industrial adoption of formal methods. In Event-B, a significant proportion of proof obligations which require human interaction fall into a family called invariant preservation . In this paper we show that a rewriting technique called rippling can increase the automation of proofs in this family, and extend this technique by combining two existing approaches.

AB - Proof automation is a common bottleneck for industrial adoption of formal methods. In Event-B, a significant proportion of proof obligations which require human interaction fall into a family called invariant preservation . In this paper we show that a rewriting technique called rippling can increase the automation of proofs in this family, and extend this technique by combining two existing approaches.

KW - Event-B

KW - automated reasoning

KW - rippling

KW - lemma conjecture

U2 - 10.1007/978-3-642-28891-3_23

DO - 10.1007/978-3-642-28891-3_23

M3 - Conference contribution

SN - 978-3-642-28890-6

T3 - Lecture Notes in Computer Science

SP - 231

EP - 236

BT - NASA Formal Methods

A2 - Goodloe, Alwyn

A2 - Person, Suzette

PB - Springer

ER -

The Use of Rippling to Automate Event-B Invariant Preservation Proofs

Abstract / Description of output

Publication series

Keywords / Materials (for Non-textual outputs)

Access to Document

Fingerprint

Projects

A14FM : using A1 to aid automation of proof search in formal methods

Cite this