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 …
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 …
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 …
Improving formal methods education.
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 …