| NSF Org: |
CCF Division of Computing and Communication Foundations |
| Recipient: |
|
| Initial Amendment Date: | February 23, 2024 |
| Latest Amendment Date: | February 23, 2024 |
| Award Number: | 2348490 |
| Award Instrument: | Standard Grant |
| Program Manager: |
Anindya Banerjee
abanerje@nsf.gov (703)292-7885 CCF Division of Computing and Communication Foundations CSE Directorate for Computer and Information Science and Engineering |
| Start Date: | September 15, 2024 |
| End Date: | August 31, 2026 (Estimated) |
| Total Intended Award Amount: | $174,966.00 |
| Total Awarded Amount to Date: | $174,966.00 |
| Funds Obligated to Date: |
|
| History of Investigator: |
|
| Recipient Sponsored Research Office: |
1600 SW 4TH AVE PORTLAND OR US 97201-5508 (503)725-9900 |
| Sponsor Congressional District: |
|
| Primary Place of Performance: |
1600 SW 4TH AVE PORTLAND OR US 97201-5522 |
| Primary Place of
Performance Congressional District: |
|
| Unique Entity Identifier (UEI): |
|
| Parent UEI: |
|
| NSF Program(s): | Software & Hardware Foundation |
| Primary Program Source: |
|
| Program Reference Code(s): |
|
| Program Element Code(s): |
|
| Award Agency Code: | 4900 |
| Fund Agency Code: | 4900 |
| Assistance Listing Number(s): | 47.070 |
ABSTRACT
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.
Please report errors in award information by writing to: awardsearch@nsf.gov.
