University of Twente Student Theses
Formal verification of a sequential SCC algorithm
Boerman, J.G.J. (2023) Formal verification of a sequential SCC algorithm.
|
PDF
1MB |
| 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: | https://purl.utwente.nl/essays/94474 |
| 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