Integration of Automatic Theorem Provers in Event-B Patterns

Event-B is a formal method for the system level modeling and analysis of dependable applications. It issupported by an open and extendable Eclipse-based tool set called Rodin. In this paper we proposed usingAutomatic theorem provers known as SMT-solvers with event-B pattern. The benefits of that are to reducethe proving effort, to reuse a model and to increase the degree of automation. The proposed approach hasbeen applied successfully on two different case studies.