University of Twente Student Theses

Login

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

Janssen, Dylan Damian (2024) Design and Implementation of new features for Runtime Permission Verification in Concurrent Java Programs using VerCors.

[img] PDF
10MB
Abstract: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.
Item Type:Essay (Master)
Clients:
Alten NL B.V., Apeldoorn, Netherlands
Faculty:EEMCS: Electrical Engineering, Mathematics and Computer Science
Subject:54 computer science
Programme:Computer Science MSc (60300)
Link to this item:https://purl.utwente.nl/essays/98745
Export this item as:BibTeX
EndNote
HTML Citation
Reference Manager

 

Repository Staff Only: item control page