Verifying Separation Logic Contracts in Chalice

Introduction

Two of the most challenging aspects of formal program verification, are framing (how to determine which assertions can be soundly preserved across, say, a method call) and handling concurrency (in particular, concurrent access to the heap). Two different approaches which have been used to tackle these problems are Separation Logic and Implicit Dynamic Frames. Both approaches involve custom assertion languages, which include constructs for controlling access to local parts of the heap (for example, via permissions). In recent work, Matthew Parkinson and Alex Summers showed how these two different approaches can be directly related to each other, by translations between Separation Logic assertions and those of Implicit Dynamic Frames. The aim of this project is to exploit this translation in order to reuse existing tool support.

Many program verification logics based on the two approaches have already been implemented. VeriFast is a tool based on Separation Logic, which gives extensive support to C and Java features. Chalice is a tool based on Implicit Dynamic Frames which tackles concurrent programs using a theorem prover. So far, it has been believed that Separation Logic cannot be directly handled by automatic theorem provers, but we aim for this!

Goal

The goal of this project is to implement a translation between VeriFast code and Chalice code. The first main step will be to identify a suitable subset of the VeriFast language to support. Then, a tool should be written to translate between one syntax and the other. In the case of some assertions (particularly, predicates in the assertion language) this translation is non-trivial. The implementation can then be used to evaluate how well the Chalice tool can deal with the corresponding examples.

If the project is chosen at the Master’s level, extra work would include investigating how to extend our translation to handle a broader class of examples, and how to add support to mimic certain automatic features in VeriFast (for example, the automatic folding and unfolding of predicate definitions, in certain cases). An inverse translation could also be attempted, which would allow for richer comparisons between the capacities of the two tools and their underlying formalisms.
Recommended Background
•    Interest in Formal Methods / Program Verification
•    Programming Experience (particularly compilers/interpreters/parsing)
•    Advantageous (but not essential) to have experience with contracts/separation logic (e.g., Software Verification master’s course)

Contact

Alex Summers