University of Twente Student Theses


Formal verification of a sequential SCC algorithm

Boerman, J.G.J. (2023) Formal verification of a sequential SCC algorithm.

[img] PDF
Abstract:Correctness of software is becoming an increasingly important subject in today's age where software becomes more and more ubiquitous. As opposed to software testing where software is executed to test correct behaviour in only a limited number of scenarios, we apply deductive verification - a technique which allows us to prove with certainty that the software is programmed correctly for all possible scenarios. In this thesis we zoom in on a Strongly Connected Components algorithm that is used inside model checkers. We formally verify a set of correctness properties that should be satisfied by the algorithm. To achieve this we use the deductive verifier VerCors which is able to statically verify assertions formulated using first-order logic formulas. We discuss our approach and proofs, and reflect on the limitations and issues that were encountered in the process. We also discuss how these issues could be addressed. Lastly, we briefly touch on how our approach would need to be adjusted to verify the parallel version of this algorithm.
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