Incremental Testing of VerCors

title:Incremental Testing of VerCors
keywords:Testing, Verification
topics:Languages, Testing
contact:W.H.M. Oortwijn MSc & S. Darabi MSc & prof.dr. M. Huisman
to be started:any time


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 design and develop such a framework. 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, the framework 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)