Thesis Topics

I am looking for motivated students interested in formal verification, interactive theorem proving, verified compilers, and AI-assisted proof mechanization. Below are some available thesis topics. If you are interested, please get in touch.

Verified Transformations on Demand for the λANF Pipeline

Master’s thesis

Develop and verify a function-specialization pass for CertiRocq's λANF pipeline, using LLMs to adapt existing Rocq proofs. Evaluate compiler performance and the human guidance needed to build new verified optimizations. proposal (PDF)

LLM-Assisted Verification of C Code Generation

Master’s thesis

Design a logical relation between CertiRocq's λANF language and CompCert's Clight, and use it to verify the C code-generation pass in Rocq under explicit runtime assumptions. Explore how LLMs can assist with both the proof's invariants and its mechanization. proposal (PDF)

Verified Library Implementations in Lean

Master’s thesis

Develop verified implementations of data structures and algorithms in the Lean proof assistant, with extraction to mainstream languages via foreign function interfaces. Requires familiarity with functional programming and interest in theorem proving.

More topics available upon request. Feel free to propose your own if it aligns with the group’s research interests.