Discharging Event-B Proof Obligations
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 ﬁrst-order logic to formulate proof obligations. This thesis shows, how the set-theoretic proof obligations from Event-B can be expressed in ﬁrst-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.