Edinburgh Research Explorer

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

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

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
StatePublished - 2012

Publication series

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

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.

Research areas

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

Download statistics

No data available

ID: 4688123