Formal Methods Accessibility

Despite their abilities, formal methods are not commonly used in industry and often remain of pure academic interest. This is, at least to some extend, caused by the complexity of mathematical notations and the inaccessibility of tools. In this project we aim to lower barriers and learning curves to enable the usage of formal methods in mainstream software industries, by regular developers.

Avatar
Sebastian Krings
Postdoc

My research interests include formal methods, model checking and logic programming.

Publications

Employing formal methods for software development usually involves using a multitude of tools such as model checkers and provers. Most …

Writing a formal model is a complicated and time-consuming task. Usually, one successively refines a model with the help of proof, …

Event-B provides a concise mathematical language for specifying invariants and guards. While both Event-B and Rodin matured, certain …

When using B or Event-B for formal specifications, model checking is often used to detect errors such as invariant violations, …

Most state-based formal methods, like B, Event-B or Z, provide support for static typing. However, these methods and the associated …

Over the years, ProB has moved from a tool that complemented proving, to a development environment that is now sometimes used instead …

Most state-based formal methods, like B, Event-B or Z, provide support for static typing. However, these methods and the associated …