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

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

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.