Verification of a model checking algorithm in VerCors

Deductive software verification is a formal method to verify that the behaviour of a program satisfies a set of specifications. We are currently able to make use of highly automated techniques to verify complex programs, such as model checking algorithms. These model checking algorithms are high-level graph algorithms which are used to reason about the behaviour of software, by verifying properties of an abstract model of the software system. Because these model checking algorithms are becoming increasingly complex, the need for formal verification of the algorithms becomes more apparent. In this thesis we show how the VerCors tool set can be used to verify a sequential model checking algorithm, the set-based SCC algorithm. We then explore how the VerCors tool set can be improved for verifying these kinds of algorithms, both by reflecting on the verification in this thesis and by comparing different related verification techniques.