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, you are asked to investigate how to further improve the use the VerCors tool set for the verification of other (parallel) graph algorithms. Possible points for improvement are:  - 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