Following other departments' traditions, we are archiving the abstracts and reading lists (and in some cases slides from the talk, and the questions the committee asks in the oral exam) for general exams in the programming languages group on this page.

Student Title Date Committee
Santiago Cuellar Inlining Compositional CompCert January 2015 Appel, Gupta, Walker link
Olivier Savary BĂ©langer Verifying an optimizing compiler May 2016 Appel, Gupta, August link
Zoe Paraskevopoulou Formal verification of closure conversion October 2016 Appel, Walker, Kincaid link
Anders Miltner Synthesizing bijective string transformers January 2017 Walker, Kincaid, Kernighan link
Nick Giannarakis Semantics of well synchronized programs on weakly consistent machines January 2017 Appel, Martonosi, Walker link
Charlie Murphy A practical algorithm for structure embedding January 2018 Kincaid, Gupta, Walker link
Matthew Z. Weaver Bicubical directed type theory May 2018 Licata, Appel, Kincaid, Walker link
Lauren Pick Exploiting synchrony and symmetry in relational verification May 2018 Gupta, Kincaid, Beringer link
Jake Silverman Loop summarization with rational vector addition systems May 2019 Kincaid, Gupta, Appel link
Qinshi Wang Decision procedures useful in separation-logic proofs of functional correctness May 2019 Appel, Kincaid, Gupta link
Devon Loehr A hiding algorithm for automatically discovering abstractions during network verification May 2020 Walker, Gupta, Kincaid link
Joomy Korkut Ergonomics and verification of a foreign function interface between Coq and C May 2020 Appel, Walker, August link
Shaowei Zhu A compositional and monotone approach to conditional termination of programs May 2020 Kincaid, Gupta, Appel link
Tim Alberdingk Thijm Kirigami, the verifiable art of network cutting May 2020 Gupta, Walker, Kincaid link
Akash Gaonkar Sequential abstractions of data-parallelism in hardware May 2021 Gupta, Appel, Kincaid link
Divya Raghunathan An abstraction for network control plane verification May 2021 Gupta, Walker, Rexford link
Joshua Cohen Verified forward erasure correction with Coq and VST January 2022 Appel, Gupta, Jamieson link
Nicolas Koh A theory of non-linear integer arithmetic May 2022 Kincaid, Walker, Gupta link
Andrew Johnson Flexible, line-rate flow monitoring of packet sequences May 2023 Walker, Kincaid, Gupta link
Nikhil Pimpalkhare Procedure Summarization via Vector Addition Systems and Inductive Linear Bounds October 5, 2023 Kincaid, Walker, Gupta link