Formal Methods Accessibility
Sep 26, 2018
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.
Sebastian Krings
Software Engineer
My interests include software analysis, formal methods and offensive security.
Related
Publications
Prototyping Games Using Formal Methods
Courses on formal methods are often based on examples and case studies, supposed to show students how to apply formal methods in …
Sebastian Krings, Philipp Körner
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 …
Sebastian Krings, Michael Leuschel
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 …
Sebastian Krings, Michael Leuschel