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

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.