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.

Model Checking Formal Methods
Sebastian Krings
Sebastian Krings
Software Engineer

My interests include software analysis, formal methods and offensive security.

Publications

Experience Report on a Student-Organized AI Course
As curricula are mostly centered around the specializations of faculty members, students are often seen purely as consumers of …
PDF Project Project Slides
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 …
PDF Project Project Slides
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 …
PDF Cite Project Project DOI
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, …
PDF Cite Project Project DOI
Meta-Predicate for Rodin
Event-B provides a concise mathematical language for specifying invariants and guards. While both Event-B and Rodin matured, certain …
PDF Cite Project
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, …
PDF Cite Project Project DOI
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 …
PDF Cite Project Project DOI
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 …
PDF Cite Project Project DOI
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 …
PDF Cite Project Project DOI