Generation of permission annotations

title:Generation of permission annotations
topics:Logics and semantics
contact:prof.dr. M. Huisman
to be started:any time


An important basis for the verification of concurrent software is the use of read and write access permissions, as used in permission-based separation logic. However, this requires the programmer to add many annotations that describe what permissions are needed by a method, and what permissions are returned. Many of these annotations seem quite obvious, and having to write them explicitly is annoying, error-prone, and time-consuming.

At VMCAI 2012, P. Ferrara and P. Müller proposed a technique to automatically generate these permissions: Automatic inference of access permissions.

Goal of this project is to integrate this inference method with our VerCors tool set for the verification of concurrent software.

In particular, the following steps are expected:

  • Understand the precision of the existing implementation by evaluating it on several examples
  • The analysis as described in this paper works on a Scala-like language; investigate what changes are necessary to make it work for Java programs and/or OpenCL kernels.
  • Investigate whether the approach can be extended for specifications, so users do not have to write access permissions for expressions used in pre- and postconditions, but instead can infer them in such a way that the specifications become self-framing.
  • For failing cases, investigate how the analysis can be improved, or extra information can be used to improve the quality of the results.