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.

翻译：Toman等人提出了一种用于自动验证低级程序的类型系统，该类型系统结合了所有权类型和精化类型，以在存在指针别名的情况下实现精化类型的强更新。我们扩展了该类型系统以支持指针算术，并证明了其可靠性。基于所提出的类型系统，我们实现了一个原型工具，用于自动验证包含指针算术的低级程序是否存在断言错误，并通过实验确认了其有效性。