A Testing Framework for a Tool Set for Program Verification

title:A Testing Framework for a Tool Set for Program Verification
contact:prof.dr. M. Huisman & W.H.M. Oortwijn MSc
to be started:any time


Goal of the VerCors tool set, developed in the FMT group at the University of Twente, is to support the verification of concurrent software. Its setup is quite ambitious, as it supports the verification of many different language features, and also the verification of programs written in many different languages.

The VerCors tool set is still under development. One bottleneck in the development process is the testing process. A large test suite is available, and applying all tests can easily take an hour. Therefore, adding a new feature, or fixing a bug easily can take up a full day (including a large amount of waiting time). Moreover, the test suite is large, but not build up very systematically, and sometimes a bug is introduced that is not caught by our tests.

In this design project, we ask you to build infrastructure to improve the testing process for VerCors. Anything that helps to reduce the waiting time will be helpful. We have some ideas how this could be done, but you will also be free to add your own ideas:

  • identify which tests are more likely to fail (by statistical analysis, analysing code changes, or ...), and apply those tests firsts
  • provide options to dynamically identify the test suite that will be used
  • provide information about part of the code that is not covered by tests
  • trigger warnings when changed code is not tested
  • use information from failing tests to propose code fixes