Ownership Types for Verification of Programs with Pointer Arithmetic
Programming Languages
2023-12-12 v1
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.
Cite
@article{arxiv.2312.06455,
title = {Ownership Types for Verification of Programs with Pointer Arithmetic},
author = {Izumi Tanaka and Ken Sakayori and Naoki Kobayashi},
journal= {arXiv preprint arXiv:2312.06455},
year = {2023}
}
Comments
An extended version of the paper to appear in Proceedings of PEPM 2024