SHF: Small: Collaborative research: Language-Integrated Verification for Determininistic Parallelism

形式化验证承诺交付的软件可以根据给定的数学规范精确地工作。在过去的十年里，已经有几个令人印象深刻的经过正式验证的软件工件，它们可以证明没有大类的缺陷。然而，这些工件需要巨大的工程壮举，使用专门的证明助手，这些助手与用于设计高效并行软件的遗留语言和库有很大的差距。该项目的新颖之处在于新技术，使有效的并行计算系统的发展与正式保证的正确性和可靠性。这个项目的影响将使形式验证成为主流软件开发的一部分。第一个是精化反射，它将现有的编程语言变成定理证明器，其中的证明仅仅是同一语言中的程序。其次，研究人员引入了格变量，调度算法和一个新的线性类型的系统，以简化高效的并行软件的建设与定义良好的行为。该项目将联合收割机的上述想法结合到一个框架中，其中工程师可以开发和验证并行软件，只需编写程序，在他们的主机语言，从而经济地集成在现有的软件开发周期的正式证明。该奖项反映了NSF的法定使命，并已被认为是值得支持的评估使用基金会的智力价值和更广泛的影响审查标准。

Formal verification promises to deliver software that works precisely according to a given mathematical specification. The last decade has seen several impressive formally verified software artifacts that are provably free of large classes of defects. However, these artifacts required Herculean feats of engineering, using specialized proof assistants that are separated, by a wide chasm, from the legacy languages and libraries that are used to engineer efficient parallel software. This project's novelties are in new techniques to enable the development of efficient parallel computing systems with formal assurances about correctness and reliability. This project's impacts will be to make formal verification a part of mainstream software development.This project will build on two approaches discovered by the investigators. The first is refinement reflection, which turns existing programming languages into theorem provers, where the proofs are merely programs in that same language. Second, the investigators have introduced lattice variables, scheduling algorithms and a new linear type system to simplify the construction of efficient parallel software with well-defined behavior. This project will combine the above ideas into a framework wherein engineers can develop and verify parallel software, simply by writing programs in their host language, thereby economically integrating formal proofs within existing software development cycles.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.