Description

Within the FMT group, we are developing the VerCors tool set for the verification of concurrent and distributed software. To demonstrate the usability of our verification technique, we have recently used it to verify the correctness of a parallel nested depth first search algorithm, which can be used for reachability analysis in model checking.

In this project, we will investigate the verification of the Set-Based SCC Algorithm using the VerCors tool set. The results of this verification will be used to identify and contribute to possible points for improvement for VerCors, such as : 

- developing a library of suitable, reusable graph properties,
- automatic generation of graph-related annotations for the algorithm,
-identifying the best way to represent graphs.
- refining the verification of a high-level algorithm into a verified, efficient implementation.

During this project you will take the following steps:
- understand program verification using VerCors
- identify a suitable (parallel) model checking algorithm
- formalise the desired correctness properties
- prove correctness of the high-level algorithm w.r.t. the desired correctness properties using the VerCors tool set
- investigate how to turn the verification into reusable results