View Proposal

---

Proposer

Kathrin Stark

Title

Verification of Compiler Optimizations

Goal

Description

Compiler optimization is the process of improving the performance of a compiler-generated code by applying a series of transformations to the code. For realistic programs, verifying rich specifications beyond shallow properties such as no out-of-bound array subscripts in a fully automated way is challenging due to the immense search space. Interactive proof assistants such as Coq or Isabelle allow humans to fill in where fully automated methods fail by allowing such proofs to be developed in an interaction between humans and computers. For this reason, proof assistants have recently gained importance also in industrial applications and are used by companies like Microsoft, Amazon, Apple, and Google. In this project, you will work on proving the correctness of optimization steps in a compiler using the Coq proof assistant. Your work will involve implementing and verifiy the optimization steps in the proof assistant, formalizing their correctness proofs, and documenting your findings. If you are interested in this project or would like to discuss your own project ideas, please contact me at [k.stark@hw.ac.uk](mailto:k.stark@hw.ac.uk) or make a short appointment at https://outlook.office365.com/owa/calendar/KathrinsMeetingCalendar@heriotwatt.onmicrosoft.com/bookings/.

Resources

Background

Url

Difficulty Level

Variable

Ethical Approval

None

Number Of Students

1

Supervisor

Kathrin Stark

Keywords

Degrees