Description

The VerCors toolset can be used to verify memory safety and functional correctness of concurrent programs written in e.g. Java, OpenCL, OpenMP, and C. Notably, VerCors focuses on verifying different concurrent models (e.g. heterogenous- and homogeneous threading) of programs written in different languages (e.g. GPU kernels, fork/join parallelism, and deterministic parallelism). The VerCors toolset is developed at the University of Twente and is actively maintained. However, making changes/updates to VerCors to solve bugs or to implement new features may easily break other existing features. The VerCors project would benefit from a framework for incremental testing: do changes made to the project break other parts of the project?

In this project you will develop an approach to systematically program verification tools. In particular, you will think about: what features to test, how to test them, and how to integrate the testing framework into project development. Ideally, this would result in a test suite of simple example programs (some of which should be verifiable, some of which should NOT be verifiable) which would be usable for VerCors, but also for other program verification tool sets.

References

1. The VerCors Tool for Verification of Concurrent Programs (Digital version available here)