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 2023 | Kincaid, Walker, Gupta | link |
| Deyuan (Mike) He | Equality saturation: Term extraction and an application to network synthesis | April 2024 | Gupta, Appel, Milano | link |