用于低延迟环境的可扩展类型状态分析
Scalable Typestate Analysis for Low-Latency Environments
摘要：
基于类型状态的静态分析在验证代码契约的正确性方面非常重要。这种分析依赖于确定性有限自动机（DFA）来指定对象的属性。我们的目标是在低延迟环境中分析合同，在这种环境中，许多有用的合同无法编码为DFA和/或其相关DFA的大小导致低于标准的性能。为了解决这个瓶颈，我们提出了一个轻量级的typestate分析器，基于一个表达规约语言，可以简洁地指定代码合同。通过实现它在静态分析器推断，我们表现出相当大的性能和可用性的好处相比，现有的技术。一个核心的见解是依赖于具有有效位向量操作的DFA的子类。
英文摘要：
Static analyses based on typestates are important in certifying correctness of code contracts. Such analyses rely on Deterministic Finite Automata (DFAs) to specify properties of an object. We target the analysis of contracts in low-latency environments, where many useful contracts are impractical to codify as DFAs and/or the size of their associated DFAs leads to sub-par performance. To address this bottleneck, we present a lightweight typestate analyzer, based on an expressive specification language that can succinctly specify code contracts. By implementing it in the static analyzer Infer, we demonstrate considerable performance and usability benefits when compared to existing techniques. A central insight is to rely on a sub-class of DFAs with efficient bit-vector operations.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
