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
Pages (from-to)95-129
Number of pages35
JournalFormal Aspects of Computing
Volume31
Issue number1
Early online date2 Jan 2019
DOIs
Publication statusPublished - Feb 2019

    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