PM Student Projects - Christoph Studer

Current ownership based verification approaches either enforce the ownership restrictions using a type checker or translate them into axioms and theorems, which are then enforced using a theorem prover. The object store is, however, modeled as one global heap, disregarding all structural information from the ownership type system.

The goal of this thesis is to define and evaluate a technique which preserves structural information from the ownership type system by conceptually splitting the global heap into smaller heaps for verification.

We believe that encoding the structural information on a heap level is simpler and more efficient than current approaches. With heap splitting, theorems and axioms encoding the ownership type system can be removed, and some proofs can be simplified because of more confined heaps.