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.

翻译：具有引用（即指针）的命令式程序的功能正确性自动验证因引用别名而具有挑战性。所有权类型近期被用于解决该问题，但现有方法存在局限性，仅对遵循特定引用使用风格的程序有效。为突破这一限制，我们融合了ConSORT（基于分数所有权）和RustHorn（基于可借用所有权）这两种基于所有权类型的自动化程序验证方法，提出了可借用分数所有权类型的概念。我们形式化了基于可借用分数所有权类型的新型类型系统，并展示了如何利用该类型系统将带引用的命令式程序的验证问题自动归约至无引用的函数式程序的验证问题。我们还证明了类型系统及翻译过程的可靠性，并通过实验验证了该方法的有效性。