The John C. Reynolds Doctoral Dissertation Award recognizes the contributions to computer science that John C. Reynolds made during his life. It is a renaming of the SIGPLAN Outstanding Doctoral Dissertation Award to encourage the clarity and rigor that Reynolds embodied and at the same time provide a reminder of Reynolds’s legacy and the difference a person can make in the field of programming language research.
The award is presented annually to the author of an outstanding doctoral dissertation in the area of programming languages.
Honorable Mention went to Zachary Kincaid (PhD 2016), supervisor Azadeh Farzan, for "Parallel Proofs for Parallel Programs". Kincaid is currently an assistant professor at Princeton University.
The citation reads:
This thesis proposes a new solution for the problem of concurrent program verification introducing the use of explicitly parallel models and logics to represent and reason about concurrent programs. An effective way of finding a sweet spot in the cost-precision spectrum is provided, weaving together the two steps of constraint generation and cons traint resolution, offering a new way to think about proofs of concurrent programs. This paradigm shift has been missing in the space of “automated” program verification of infinite-state programs, since despite the absolute elegance of Owicki-Gries and Rely-Guarantee proof techniques, the completeness of these techniques heavily relies on the concept of auxiliary proof state. In this thesis, “inductive data flow graphs” (iDFG) offer the same completeness and elegance as the Owicki-Gries method minus the need for the auxiliary state in generating provably “compact” proof arguments. The elegance of iDFGs are generalized into a proof method “proof spaces” for concurrent programs with “unboundedly” many threads.