Increasing Student Self-Reliance and Engagement in Model-Checking Courses
Courses on formal methods focus on two aspects: teaching formalisms and exemplary applications as well as teaching techniques for implementing tools such as model checkers.
Model Checking
A Verified Low-Level Implementation of the Adaptive Exterior Light and Speed Control System
ABZ 2021 – 8th International Conference on Rigorous State Based Methods, virtual
Testing, Model Checking and Static Analysis – Dream Team or Rivals?
Ensuring reliability and quality of software has become a necessity.
Testing, Model Checking and Static Analysis – Dream Team or Rivals?
Embedded World Conference 2020, virtual
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 instead.
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.
Translating Alloy and Extensions to Classical B
In this article, we introduce a denotational translation of the specification language Alloy to classical B.
Inquiry- and Research-based Teaching in a Course on Model Checking
FMFun 2019, Bergen, Norway
Prototyping Games using Formal Methods
FMFun 2019, Bergen, Norway
Inquiry- and Research-based Teaching in a Course on Model Checking
In this presentation, we discuss a recent publication on our course on model checking.
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.
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.
A Translation from Alloy to B
In this paper, we introduce a translation of the specification language Alloy to classical B.
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.
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 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.
Proof Assisted Symbolic Model Checking for B and Event-B
We have implemented various symbolic model checking algorithms, like BMC, k-Induction and IC3 for B and Event-B.
From Animation to Data Validation: The ProB Constraint Solver 10 Years On
Various solvers are linked via reification and Prolog co-routines.