Pldi

Two papers accepted at PLDI’23:

• Mostly Automated Proof Repair for Verified Libraries (co-authored with Kiran Gopinathan and Mayank Keoliya) presents the first proof repair methodology for verified OCaml programs that use higher-order functions.
• Leveraging Rust Types for Program Synthesis (joint work with Jonas Fiala, Shachar Itzhaky, Peter Müller, and Nadia Polikarpova) describes the first technique to synthesise Rust programs that satisfy user-provided specifications.