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 …
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 …
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 …
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 …
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 …
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 …
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 …