CRII: SHF: Embedding techniques for mechanized reasoning about existing programs

在形式化验证中，嵌入描述了如何在定理证明器中对编程语言的语法和语义进行建模。这是验证现有程序的第一步，在这一步中使用的嵌入技术对后续的机械化推理工作具有至关重要的直接影响。因此，本项目研究形式化方法中使用的嵌入技术，以机械地推断程序的功能正确性。这个项目的新颖之处在于它专注于浅嵌入，它已经被证明可以实现更简单的推理技术，以及混合嵌入，它已经被证明可以作为不同语言/工具的良好接口。该项目的影响包括提供了一个简单的框架，用于对功能正确性进行机械推理，并对嵌入技术提供了更多的见解。本项目侧重于三个任务。首先，研究者和他的团队将开发一种工具，可以将C代码转换为混合嵌入，从而实现等式推理。之后，他们将推广C程序混合嵌入的概念，以开发用C和Haskell编写的程序的统一嵌入。最后，该项目将研究基于这种统一嵌入的可转移证明的技术，以便用户可以重用用不同编程语言编写的类似程序的证明。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

In formal verification, embedding describes how to model a programming language's syntax and semantics in a theorem prover. This is the first step of verifying an existing program and the embedding techniques used in this step have crucial direct impacts on the subsequent mechanized reasoning effort. Therefore, this project studies the embedding techniques used in formal methods to mechanically reason about a program's functional correctness. The project's novelties are its focus on shallow embeddings, which have been shown to enable simpler reasoning techniques, and mixed embeddings, which have been shown to serve as a good interface for different languages/tools. The project's impacts include providing a simple framework for mechanically reasoning about functional correctness as well as providing more insight into embedding techniques.This project focuses on three tasks. First, the investigator and his group will develop a tool that translates C code to mixed embeddings that enable equational reasoning. After that, they will generalize the concept of mixed embeddings for C programs to develop a unified embedding for programs written in C and Haskell. Finally, this project will study techniques that enable transferable proofs based on this unified embedding so that a user can reuse proofs for similar programs written in different programming languages.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.