Logik und Formale Methoden

Discharging Event-B Proof Obligations

  • Links:PDF
    Presentation (PDF)
  • In this thesis, a concept for the discharging of Event-B proof obligations using the KeY tool is presented. While Event-B makes use of a set-theoretic notation, KeY uses first-order logic to formulate proof obligations. This thesis shows, how the set-theoretic proof obligations from Event-B can be expressed in first-order logic and be translated to the KeY input language. In the next step, an approach for the discharging of these proof obligations in the KeY tool is formulated and extended to achieve a high level of automation. The overall approach is shown to be promising with help of a case study. It was even possible to discharge more proof obligations automatically with help of the KeY prover than within the Rodin toolset for Event-B modeling.

Bibtex entry for this thesis

author = {Christopher K{\"o}ker},
title = {Discharging {Event-B} Proof Obligations},
howpublished = {Studienarbeit, Fakult{\"a}t f{\"u}r Informatik, Universit{\"a}t Karlsruhe},
month = {September},
year = {2008},
keywords = {Event-B, KeY}