SHF:Small:Analysis, Repair, and Synthesis for k-Safety

该项目旨在消除一大类软件错误，称为k-安全错误，这些错误是由同一过程的多次不一致执行引起的。虽然在自动检测此类错误方面的工作相对较少，但调查人员在广泛使用的软件项目中发现了数十个此类错误。这个项目开发了语义推理技术，帮助软件工程师实现正确的程序，而不会出现k-安全错误。除了提高多种软件的安全性和可靠性外，这些技术还使软件工程师可以更轻松地开发、维护和调试他们的项目。在这个项目中产生的工具和技术将是开源的，并尽可能纳入教育课程。该项目包括研究生和本科生。该项目开发了一个全面的理论框架，用于推理任意k-安全属性，包括结合性、决定论、传递性和其他性质。基于笛卡尔-霍尔逻辑(CHL)的初步工作，研究人员探索了一系列用于k-安全的语义推理工具，从静态和动态分析到自动修复和综合。在分析方面，该项目探索了精确和可伸缩的静态分析技术，这些技术可以使用自动推断的关系程序不变量来自动证明不存在k安全违规。该项目还调查了静态和动态相结合的程序分析技术，这些技术可以为k-安全违规行为提供证据。

This project aims to eradicate a broad class of software bugs, called k-safety errors, that arise from multiple inconsistent executions of the same procedure. While there is relatively little work on automated detection of such errors, the investigators have found dozens of such errors in widely-used software projects. This project develops semantic reasoning techniques that help software engineers implement correct programs that do not exhibit k-safety errors. In addition to improving the security and reliability of many kinds of software, these techniques make it easier for software engineers to develop, maintain, and debug their projects. The tools and techniques generated in this project will open-source and incorporated into the educational curriculum whenever possible. The project includes graduate and undergraduate students in this research. The project develops a comprehensive theoretical framework for reasoning about arbitrary k-safety properties, including associativity, determinism, transitivity, and others. Based on preliminary work on Cartesian Hoare Logic (CHL), the investigators explore a wide range of semantic reasoning tools for k-safety, ranging from static and dynamic analysis to automated repair and synthesis. On the analysis side, the project explores precise and scalable static analysis techniques that can automatically prove the absence of k-safety violations using automatically inferred relational program invariants. The project also investigates combined static and dynamic program analysis techniques that can provide witnesses to k-safety violations.