Description

Recently, a quantitative separation logic to reason about probabilistic pointer programs has been proposed. In Twente we are developing the VerCors program verifier, which uses separation logic to reason about (concurrent) programs. In this project, we would like to investigate how we could adapt the set up of the VerCors verifier such that it could support this quantitative separation logic.

The following steps would be necessary:

• understand the quantitative separation logic
• understand the VerCors architecture
• investigate how to adapt the VerCors architecture such that it could support quantitative separation logic
• implement the necessary changes