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的法定任务，并被认为是值得通过基金会的知识分子优点和更广泛的审查标准通过评估来获得支持的。