Collaborative Research: SHF: Small: Lightweight Modular Typestate

软件可靠性对社会至关重要，软件验证者可以通过保证没有某些错误来提高可靠性。特别是，类型状态验证通过确保程序不执行某些非法操作序列来防止重要的错误类别。然而，尽管经过了30多年的研究，类型状态验证并没有被开发人员广泛采用。该项目将开发轻量级类型状态验证技术，利用对类型状态属性结构和公共编程模式的新见解。该项目预计将使程序员更容易采用类型状态验证，从而提高大型真实软件系统的可靠性。采用类型状态分析的一个关键障碍是处理指针别名，在现有方法中，这需要进行昂贵的整个程序分析，或者在模块化方法中，需要重量级代码注释。该项目将通过开发利用现代代码库中的类型状态系统特征和常见别名模式的算法来实现轻量级和模块化的类型状态验证。例如，该项目确定了累加类型状态系统，在该系统中，对象启用的方法只会随着时间的推移而增长。即使在没有别名信息的情况下，累加类型状态系统也可以被很好地验证。该项目还研究了由流畅API等现代编码模式产生的受限别名模式，这些模式可以使用轻量级、模块化技术进行精确分析。该项目将把这些见解应用于传统的类型状态系统和现有类型状态形式中不方便或不可能表达的新属性。该奖项反映了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.