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

Automated Backend Selection for ProB Using Deep Learning

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

Repair and Generation of Formal Models Using Synthesis

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

Meta-Predicate for Rodin

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

Interactive Model Repair by Synthesis

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

Inferring Physical Units in Formal Models

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

Who watches the watchers: Validating the ProB Validation Tool

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

Inferring Physical Units in B Models

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