Skip to content

Research at St Andrews

Automating Event-B invariant proofs by rippling and proof patching

Research output: Contribution to journalArticle

Author(s)

Yuhui Lin, Alan Bundy, Gudmund Grov, Ewen Maclean

School/Research organisations

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.
Close

Details

Original languageEnglish
Number of pages35
JournalFormal Aspects of Computing
VolumeFirst Online
Early online date2 Feb 2019
DOIs
StateAccepted/In press - 11 Dec 2018

    Research areas

  • Formal Verification, Event-B, Automated Reasoning, Rippling, Lemma conjecturing

Discover related content
Find related publications, people, projects and more using interactive charts.

View graph of relations

Related by journal

  1. Formal verification of a pervasive messaging system

    Konur, S., Fisher, M., Dobson, S. A. & Knox, S. Apr 2014 In : Formal Aspects of Computing. 26, 4, p. 677-694 18 p.

    Research output: Contribution to journalArticle

  2. Applications of real number theorem proving in PVS

    Gottliebsen, H., Hardy, R., Lightfoot, O. & Martin, U. Nov 2013 In : Formal Aspects of Computing. 25, 6, p. 993-1016 24 p.

    Research output: Contribution to journalArticle

ID: 256910422