- Author
- Lin, Yuhui
- Bundy, Alan
- Grov, Gudmund
- Maclean, Ewen
- Date Issued
- 2019-01-02
- Keywords
- Automatisk resonnering
- Automatisering
- Analyseverktøy
- Permalink
- http://hdl.handle.net/123456789/77395
- http://hdl.handle.net/20.500.12242/2518
- DOI
- 10.1007/s00165-018-00476-7
- Collection
- Articles
- Description
- Lin, Yuhui; Bundy, Alan; Grov, Gudmund; Maclean, Ewen. Automating Event-B invariant proofs by rippling and proof patching. Formal Aspects of Computing 2019 s. 1-35
-
- 1653322
- Size: 799k
- 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.