ConSORT：面向命令式程序的上下文与流敏感所有权精化类型
ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs
AI总结：
该研究提出ConSORT类型系统，结合精化类型与分数所有权类型，解决命令式程序中别名导致的强更新判定难题，实现自动推理工具，可验证含数据结构的非平凡程序。
摘要：
我们提出了ConSORT，这是一种适用于存在可变性与别名情况的安全验证类型系统。可变性要求强更新以对程序执行过程中变化的不变量进行建模，但指针间的别名使得难以确定哪些不变量需随变更更新。我们的类型系统通过精化类型与分数所有权类型的新颖组合解决了这一难题：分数所有权类型为引用变量提供流敏感且精确的别名信息，ConSORT利用该所有权信息可靠处理潜在别名引用的强更新。我们已证明ConSORT的可靠性并实现了完全自动推理工具的原型，对该工具的评估显示其可验证包括数据结构实现在内的非平凡程序。
英文摘要：
We present ConSORT, a type system for safety verification in the presence of mutability and aliasing. Mutability requires strong updates to model changing invariants during program execution, but aliasing between pointers makes it difficult to determine which invariants must be updated in response to mutation. Our type system addresses this difficulty with a novel combination of refinement types and fractional ownership types. Fractional ownership types provide flow-sensitive and precise aliasing information for reference variables. ConSORT interprets this ownership information to soundly handle strong updates of potentially aliased references. We have proved ConSORT sound and implemented a prototype, fully automated inference tool. We evaluated our tool and found it verifies non-trivial programs including data structure implementations.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
