Experience Report on An Inquiry-Based Course on Model Checking

Abstract

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 inside well-known model checkers which have been in development for many years. This is seldom taken into account by university courses on the topic, which often remain on the theoretical level. Hence, they do not provide practical access to the topic for reasons such as lack of time or inaccessibility of tools and their source code. In this article, we present a recent revision of our course on model checking, shifting from a classical lecture-based format to inquiry and research-based teaching. We document course development, present some didactic methods used and evaluate the course based on peer review and student feedback. Furthermore, we try to assert student engagement empirically.