Christian Haack,
Radboud Universiteit Nijmegen

Specification and verification of heap access policies

Abstract

Modular verification methodologies usually include constructs for specifying heap access policies, for instance, in the form of frame axioms or delimiters for blocks in which objects may be mutated. Making heap access policies explicit and verifying adherence is useful in its own right, especially in concurrent programs. For instance, read-only objects (immutable objects) can be shared between concurrent threads without synchronization.

In this course, we will discuss various techniques for specifying and checking heap access policies. These will include type-based techniques for checking object immutability, substructural type systems and logics for supporting dynamic access protocols, and an adaptation of concurrent separation logic to a Java-like setting.

• Slides for Monday's class.
• Notes on lexically scoped regions for initialization of pluggable object types.
• Slides for Wednesday's class.