Formal Methods

A Verified Low-Level Implementation of the Adaptive Exterior Light and Speed Control System

In this article, we present an approach to the ABZ 2020 case study, that differs from the ones usually presented at ABZ: Rather than using a (correct-by-construction) pproach following a formal method, we use MISRA C for a low-level implementation …

Validation and Real-Life Demonstration of ETCS Hybrid Level 3 Principles Using a Formal B Model

In this article, we present a concrete realisation of the ETCS Hybrid Level 3 concept, whose practical viability was evaluated in a field demonstration in 2017. Hybrid Level 3 introduces virtual sub-sections as sub-divisions of classical track …

Translating Alloy and Extensions to Classical B

In this article, we introduce a denotational translation of the specification language Alloy to classical B. Our translation closely follows the Alloy grammar. Each construct is translated into a semantically equivalent component of the B language. …

Embedding SMT-LIB into B for Interactive Proof and Constraint Solving

Paper presentation.

Prototyping Games using Formal Methods

Paper presentation.

Inquiry- and Research-based Teaching in a Course on Model Checking

Paper presentation.

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 practice. However, examples often fall into one of two categories: First, many are artificial and thus do not relate to …

Embedding High-Level Formal Specifications into Applications

The common formal methods workflow consists of formalising a model followed by applying model checking and proof techniques. Once an appropriate level of certainty is reached, code generators are used in order to gain executable code. In this paper, …

The History and Evolution of B and Event-B

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 of them again feature different backends and configuration options. Selecting an appropriate configuration for a …