Edinburgh Research Archive logo

Edinburgh Research Archive

University of Edinburgh homecrest
View Item 
  •   ERA Home
  • Informatics, School of
  • Informatics thesis and dissertation collection
  • View Item
  •   ERA Home
  • Informatics, School of
  • Informatics thesis and dissertation collection
  • View Item
  • Login
JavaScript is disabled for your browser. Some features of this site may not work without it.

Use of rippling to automate Event-B invariant preservation proofs

View/Open
Lin2015.pdf (1.774Mb)
Date
29/06/2015
Item status
Restricted Access
Embargo end date
31/12/2100
Author
Lin, Yu Hui
Metadata
Show full item record
Abstract
The use of formal method techniques can contribute to the production of more reliable and dependable systems. However, a common bottleneck for the industrial adoption of formal methods techniques is proof automation. To address the challenge of proof automation, we aim to improve it by using automated theorem proving techniques. We set one popular formal method technique as our working domain in this thesis, that is, Event-B. More specifically, we target a family of proofs, i.e. invariant preservation (INV) proofs, which can account for a significant part of the proofs that needs human interactions. We apply one of the most successful automated theorem proving techniques, which is rippling, to improve the proof automation of Event-B INV POs. Rippling uses metalevel guidance to automate proofs, and it is in particular useful to develop proof patches to recover proofs based on the meta-level guidance when proof attempts fail. We are especially interested in the case when lemmas are required to recover failed proofs. We combine a scheme-based theory-exploration system, i.e. IsaScheme, with rippling to develop a proof patch for lemma discovery, i.e. ahLemma. In addition to ahLemma, we also develop two proof patches to suggest case-splits and to simplify the goal and hypotheses by rewriting. The combining use of rippling and these proof patches can improve the proof automation of INV POs.
URI
http://hdl.handle.net/1842/31453
Collections
  • Informatics thesis and dissertation collection

Library & University Collections HomeUniversity of Edinburgh Information Services Home
Privacy & Cookies | Takedown Policy | Accessibility | Contact
Privacy & Cookies
Takedown Policy
Accessibility
Contact
feed RSS Feeds

RSS Feed not available for this page

 

 

All of ERACommunities & CollectionsBy Issue DateAuthorsTitlesSubjectsPublication TypeSponsorSupervisorsThis CollectionBy Issue DateAuthorsTitlesSubjectsPublication TypeSponsorSupervisors
LoginRegister

Library & University Collections HomeUniversity of Edinburgh Information Services Home
Privacy & Cookies | Takedown Policy | Accessibility | Contact
Privacy & Cookies
Takedown Policy
Accessibility
Contact
feed RSS Feeds

RSS Feed not available for this page