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


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
Number of pages6
ISBN (Electronic)978-3-642-28891-3
ISBN (Print)978-3-642-28890-6
Publication statusPublished - 2012

Publication series

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


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


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