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

CRII：SHF：现有程序机械化推理的嵌入技术

• 批准号: 2348490
• 负责人: Yao Li
• 金额: $ 17.5万
• 依托单位: Portland State University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2024
• 资助国家: 美国
• 起止时间: 2024-09-15 至 2026-08-31
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2348490&HistoricalAwards=false
• 关键词: CRII; SHF; Embedding; techniques; mechanized

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.

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