Description

When many concurrent programs use atomic operations for efficiency reasons. In order to verify such programs, we need to provide formalisations of the atomic operations. We have several papers that describe suitable formalisations for atomic operations, but we lack a standard library that we can load if we wish to verify a new algorithm using atomic operations.

The goal of this project is to develop such a library. You will be expected to take the following steps:

- study the papers that provide verification examples using atomic operations
- from these papers, distill one or more suitable formalisations of atomic operations
- provide these formalisations as standard libraries that can be reused in VerCors
- if time permits, provide a formal argument why the library specification is sound