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

Yuhui Lin, Alan Bundy, Gudmund Grov

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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.
Original languageEnglish
Title of host publicationNASA Formal Methods
Subtitle of host publication4th International Symposium, NFM 2012, Norfolk, VA, USA, April 3-5, 2012. Proceedings
EditorsAlwyn Goodloe, Suzette Person
PublisherSpringer-Verlag GmbH
Pages231-236
Number of pages6
ISBN (Electronic)978-3-642-28891-3
ISBN (Print)978-3-642-28890-6
DOIs
Publication statusPublished - 2012

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin / Heidelberg
Volume7226
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Keywords

  • Event-B
  • automated reasoning
  • rippling
  • lemma conjecture

Fingerprint

Dive into the research topics of 'The Use of Rippling to Automate Event-B Invariant Preservation Proofs'. Together they form a unique fingerprint.

Cite this