Ownership Types for Verification of Programs with Pointer Arithmetic

TL;DR

This paper extends an ownership and refinement type system for verifying low-level programs with pointer arithmetic, proving its soundness and demonstrating its effectiveness through a prototype tool and experiments.

Contribution

It introduces support for pointer arithmetic into an existing verification type system and provides a soundness proof and practical implementation.

Findings

Successfully extended the type system to handle pointer arithmetic

Proved the soundness of the extended type system

Demonstrated effectiveness with a prototype tool and experimental results

Abstract

Toman et al. have proposed a type system for automatic verification of low-level programs, which combines ownership types and refinement types to enable strong updates of refinement types in the presence of pointer aliases. We extend their type system to support pointer arithmetic, and prove its soundness. Based on the proposed type system, we have implemented a prototype tool for automated verification of the lack of assertion errors of low-level programs with pointer arithmetic, and confirmed its effectiveness through experiments.