author: Bob Rubbens
title: Extending Java support in VerCors
keywords: program verification, Java
topics: Software Technology
committee: Sophie Lathouwers ,
Marieke Huisman
started: September 2019

Description

In our group, we develop the tool VerCors [1] which is used to verify functional correctness and ensure data race-freedom in concurrent programs.

VerCors can support many different input languages. They are all transformed to the same intermediate language after which they are passed on to the tool Viper for verification. While we do offer support for Java, this support is limited at the moment. Therefore, we would like you to extend the support for Java features.

There is a list available which describes the current support for Java, some features which are not yet supported include: inheritance, variable scoping, if-statements with a single body statement, initialization of variables outside the constructor, etc.

Tasks:

  1. Decide which features you would like to add
  2. Figure out how verification support for these features should work
  3. Implement the support for this feature in the VerCors tool

References

  1. VerCors tool (Digital version available here)