Borrowable Fractional Ownership Types for Verification

TL;DR

This paper introduces borrowable fractional ownership types, combining existing ownership approaches to improve automated verification of imperative programs with references, making the process more flexible and applicable to a wider range of programs.

Contribution

It proposes a new type system based on borrowable fractional ownership types, integrating two recent ownership verification methods to enhance automation and generality.

Findings

The type system is sound and formally verified.

The approach reduces imperative program verification to functional program verification.

Experimental results confirm the effectiveness of the proposed method.

Abstract

Automated verification of functional correctness of imperative programs with references (a.k.a. pointers) is challenging because of reference aliasing. Ownership types have recently been applied to address this issue, but the existing approaches were limited in that they are effective only for a class of programs whose reference usage follows a certain style. To relax the limitation, we combine the approaches of ConSORT (based on fractional ownership) and RustHorn (based on borrowable ownership), two recent approaches to automated program verification based on ownership types, and propose the notion of borrowable fractional ownership types. We formalize a new type system based on the borrowable fractional ownership types and show how we can use it to automatically reduce the program verification problem for imperative programs with references to that for functional programs without references. We also show the soundness of our type system and the translation, and conduct experiments to confirm the effectiveness of our approach.