论文标题
consort：命令式计划的上下文和流动敏感的所有权精致类型
ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs
论文作者
论文摘要
我们介绍了Consort，这是一种在存在可变性和混叠的情况下安全验证的类型系统。 Mustability在程序执行过程中需要强大的更新才能模型更改不变性，但是指针之间的别名使得很难确定必须对突变进行更新哪些不变性。我们的类型系统通过新颖的精炼类型和分数所有权类型的新型组合解决了这一困难。分数所有权类型为参考变量提供流动敏感和精确的混叠信息。 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.
