Improving the Maintainability of a Verification Toolset

title:Improving the Maintainability of a Verification Toolset
keywords:Program verification, maintainability, concurrency, Scala, Java
contact:prof.dr. M. Huisman & W.H.M. Oortwijn MSc
to be started:any time


Description

The VerCors toolset is a verification toolset, developed and maintained at the FMT group of the University of Twente, that allows to verify concurrent and parallel software. Multiple front-end languages with concurrency features are supported, including Java, C, and PVL, the latter our prototypal verification language. To deal with multiple languages, VerCors uses an intermediate language. VerCors is essentially a set of compiler transformations over this intermediate language, which are used to translate verification problems represented as e.g. Java programs to verification problems that low-level/SMT solvers can work with. 

A lot can be done to improve on VerCors's maintainability. One key direction in this is that the AST nodes of the intermediate language are mutable; the compiler transformations mostly just alter the state of the AST. It would be more ideal to have all AST nodes immutable (e.g. represented as "case classes" in Scala), so that compiler transformations are functions that map AST's to AST's.

In this design project, we ask you to make (a part of) VerCors's intermediate language immutable and update (a part of) the compiler transformations accordingly. To do this, you need to get familiar with the basic architecture of VerCors, see [1]. 

References

  1. VerCors GitHub page (Digital version available here)