Automating Event-B invariant proofs by rippling and proof patching

Author
Lin, Yuhui
Bundy, Alan
Grov, Gudmund
Maclean, Ewen
Date Issued
2019
Keywords
Automatisk resonnering
Automatisering
Analyseverktøy
Permalink
http://hdl.handle.net/123456789/77395
http://hdl.handle.net/20.500.12242/2518
DOI
https://doi.org/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.
View Meta Data