Collaborative Research: SHF: Small: Lightweight Modular Typestate

软件可靠性对社会至关重要，软件验证者可以通过保证不存在某些错误来提高可靠性。 特别是，类型状态验证通过确保程序不执行某些非法操作序列来防止重要类别的错误。 然而，尽管经过了30多年的研究，类型状态验证还没有被开发人员广泛采用。 该项目将开发轻量级类型状态验证技术，利用对类型状态属性结构和常见编程模式的新见解。 该项目预计将使程序员更容易采用类型状态验证，从而提高大规模，真实世界的软件系统的可靠性。采用类型状态分析的一个关键障碍是处理指针别名，这在现有的方法中需要昂贵的全程序分析，或者在模块化方法中，重量级代码注释。 这个项目将通过开发利用typestate系统特性和现代代码库中常见的别名模式的算法来实现轻量级和模块化的typestate验证。 例如，该项目确定了累积类型状态系统，其中对象的启用方法只会随着时间的推移而增长。即使在没有别名信息的情况下，积累型状态系统也可以得到可靠的验证。该项目还研究了现代编码模式（如流畅的API）产生的受限别名模式，这些模式可以通过轻量级模块化技术进行精确分析。 该项目将把这些见解应用于传统的typestate系统和不方便或不可能在现有typestate形式主义中表达的新属性。该奖项反映了NSF的法定使命，并被认为值得通过使用基金会的知识价值和更广泛的影响审查标准进行评估来支持。

Software reliability is of critical importance to society, and software verifiers can improve reliability by guaranteeing the absence of certain bugs. In particular, typestate verification prevents important classes of bugs by ensuring programs do not perform certain illegal operation sequences. However, despite over 30 years of research, typestate verification has not been widely adopted by developers. This project will develop techniques for lightweight typestate verification, leveraging new insights on the structure of typestate properties and common programming patterns. The project is expected to make typestate verification significantly easier for programmers to adopt, thereby improving the reliability of large-scale, real-world software systems.A key barrier to adoption of typestate analysis is handling of pointer aliasing, which in extant approaches necessitates either an expensive whole-program analysis or, in modular approaches, heavyweight code annotations. This project will achieve lightweight and modular typestate verification by developing algorithms that leverage typestate system characteristics and common aliasing patterns in modern code bases. For example, the project identifies accumulation typestate systems, in which an object's enabled methods only grow over time. An accumulation typestate system can be verified soundly even in the absence of alias information. The project also studies restricted aliasing patterns arising from modern coding patterns like fluent APIs, which can be precisely analyzed with lightweight, modular techniques. The project will apply these insights both to traditional typestate systems and to new properties that are inconvenient or impossible to express in existing typestate formalisms.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.