Description

Within the FMT group, we are developing the VerCors tool set for the verification of concurrent and distributed software. We have developed an abstraction technique that can be used to reason about the behaviour of a concurrent or distributed program. in earlier work, we have shown that this approach is suitable to reason about a distributed leader election protocol.

In this project, you are asked to investigate the suitability of this approach for other distributed algorithms, by verifying multiple classical distributed algorithms using our abstract model approach. Ultimately, we would like to understand how we can further automate this process, for example by automatically identifying the abstract models.  Concretely, we expect you to take the following steps:

- understand program verification and abstract models as supported by VerCors
- identify classical algorithms that can be verified using this approach
- provide abstract models for these classical algoritms
- prove that the algorithm implements the abstract model for these examples
- develop techniques to further automate this process