ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs

TL;DR

ConSORT is a novel type system combining refinement and fractional ownership types to enable safe, automated verification of imperative programs with mutable, aliased references, ensuring sound handling of strong updates.

Contribution

It introduces a new type system that integrates refinement and fractional ownership types for precise, flow-sensitive aliasing and mutation reasoning in imperative programs.

Findings

Successfully verifies complex data structure implementations

Proved soundness of the type system

Automated inference tool demonstrates practical effectiveness

Abstract

We present ConSORT, a type system for safety verification in the presence of mutability and aliasing. Mutability requires strong updates to model changing invariants during program execution, but aliasing between pointers makes it difficult to determine which invariants must be updated in response to mutation. Our type system addresses this difficulty with a novel combination of refinement types and fractional ownership types. Fractional ownership types provide flow-sensitive and precise aliasing information for reference variables. ConSORT interprets this ownership information to soundly handle strong updates of potentially aliased references. We have proved ConSORT sound and implemented a prototype, fully automated inference tool. We evaluated our tool and found it verifies non-trivial programs including data structure implementations.