Design and Implementation of new features for Runtime Permission Verification in Concurrent Java Programs using VerCors

Concurrent programs increase productively significantly for computers, but they can also introduce bugs, like data races and deadlocks. VerCors is a static verification tool that can verify using formal specifications that the concurrent programs behave correctly. VerCors also wants support for runtime verification for Java programs using the same formal specifications as static verification. Gijsen implemented an initial prototype in 2015 to perform basic runtime permission checking in VerCors. However, the prototype does not work with the current version of VerCors and uses an approach that is different from the annotations from VerCors, which limits the addition of new features to the runtime checking prototype. Additionally, the prototype was only limited in its functionality, it only provides support for basic permission checking. In this master’s thesis, we will first identify how to rework the old prototype to a new prototype that does work with the current version of VerCors. Additionally, we will design and implement new features for implementing permission checking for arrays, quantifiers, loop invariants, lock invariants and predicates. We identify different options to implement the new features in the prototype and implement the mentioned features into the prototype.