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.
|
PDF
2MB |
| 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: | https://purl.utwente.nl/essays/88268 |
| Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page