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.
Formal Methods Accessibility
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 …