Model Checking

Experience Report on An Inquiry-Based Course on Model Checking

In this presentation, we discuss a recent publication on our course on model checking. The course has been shifted from a classical lecture-based format to inquiry and research-based teaching. In the article to be presented, we documented course …

Experience Report on An Inquiry-Based Course on Model Checking

The development and improvement of model checkers for the validation of hard- and software is an ongoing research topic in computer science. Model checking research connects theoretical and practical aspects; new algorithms are often implemented …

BMoth

A prototypical model checker focussing on reusable libraries.

Formal Methods Accessibility

Lower barriers and learning curves to enable the usage of formal methods in mainstream industries.

ProB

Animator, constraint solver and (symbolic) model checker for the B-Method.

Writing a Model Checker in 80 Days: Reusable Libraries and Custom Implementation

During a course on model checking we developed BMoth, a full-stack model checker for classical B, featuring both explicit-state and symbolic model checking. Given that we only had a single university term to finish the project, a particular focus was …

A Translation from Alloy to B

In this paper, we introduce a 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. In addition to …

Using a Formal B Model at Runtime in a Demonstration of the ETCS Hybrid Level 3 Concept with Real Trains

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, an evolution of the ETCS Level 2 principles, introduces Virtual …

Proof Assisted Bounded and Unbounded Symbolic Model Checking of Software and System Models

We have implemented various symbolic model checking algorithms, such as BMC, k-Induction and IC3 for B, Event-B and other modeling languages. The high-level nature of software models accounts for complicated constraints arising in these symbolic …

The Burden of High-Level Languages: Complicated Symbolic Model Checking

Symbolic model checking algorithms like IC3 have proven to be an effective technique for hardware model checking. Extensions to software model checking have been suggested and implemented and seem promising so far. However, using symbolic model …