Show simple item record

dc.contributor.advisorBundy, Alanen
dc.contributor.advisorMaclean, Ewenen
dc.contributor.advisorGudmund, Groven
dc.contributor.authorLin, Yu Huien
dc.date.accessioned2018-07-30T15:35:55Z
dc.date.available2018-07-30T15:35:55Z
dc.date.issued2015-06-29
dc.identifier.urihttp://hdl.handle.net/1842/31453
dc.description.abstractThe 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.en
dc.language.isoen
dc.publisherThe University of Edinburghen
dc.subjectEvent-Ben
dc.titleUse of rippling to automate Event-B invariant preservation proofsen
dc.typeThesis or Dissertationen
dc.type.qualificationlevelDoctoralen
dc.type.qualificationnamePhD Doctor of Philosophyen
dc.rights.embargodate2100-12-31
dcterms.accessRightsRestricted Accessen


Files in this item

This item appears in the following Collection(s)

Show simple item record