University of Twente Student Theses


Verification of a model checking algorithm in VerCors

Hollander, J.P. (2021) Verification of a model checking algorithm in VerCors.

[img] PDF
Abstract: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.
Item Type:Essay (Master)
Faculty:EEMCS: Electrical Engineering, Mathematics and Computer Science
Subject:54 computer science
Programme:Computer Science MSc (60300)
Link to this item:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page