Edinburgh Research Explorer

Automating Event-B invariant proofs by rippling and proof patching

Research output: Contribution to journalArticle

Related Edinburgh Organisations

Open Access permissions

Open

Documents

https://link.springer.com/article/10.1007%2Fs00165-018-00476-7
Original languageEnglish
Pages (from-to)1-35
Number of pages35
JournalFormal Aspects of Computing
DOIs
StatePublished - 2 Jan 2019

Abstract

The use of formal method techniques can contribute to the production of more reliable and dependable systems. However, a common bottleneck for industrial adoption of such techniques is the needs for interactive proofs. We use a popular formal method, called Event-B, as our working domain, and set invariant preservation (INV) proofs as targets, because INV proofs can account for a significant proportion of the proofs requiring human interactions. We apply an inductive theorem proving technique, called rippling, for Event-B INV proofs. Rippling automates proofs using meta-level guidance. The guidance is in particular useful to develop proof patches to recover failed proof attempts. We are interested in the case when a missing lemma is required. We combine a scheme-based theory-exploration system, called IsaScheme [MRMDB10], with rippling to develop a proof patch via lemma discovery. We also develop two new proof patches to unfold operator definitions and to suggest case-splits, respectively. The combined use of rippling with these three proof patches as a proof method significantly improves the proof automation for our evaluation set.

Download statistics

No data available

ID: 78357324