Congratulations to Rutgers CS PhD graduate David Menendez ! David Menendez's dissertation "Practical Formal Techniques and Tools for Developing LLVM's Peephole Optimizations" has been selected to receive the ACM SIGPLAN John C. Reynolds Dissertation Award. David's dissertation was supervised by Prof. Santosh Nagarakatte. David defended his dissertation in December 2017 and is available online at https://www.cs.rutgers.edu/~santosh.nagarakatte/david-menendez-phd-thesis.pdf
This award is presented annually to the author of an outstanding doctoral dissertation in the area of Programming Languages. The award includes a prize of $1,000. The awardee can choose to receive the award at ICFP, OOPSLA, POPL, or PLDI. At the discretion of the Selection Committee, multiple awards and/or honorable mentions may be presented for a given year. This year David Menendez is sharing this award with Justin Hsu.
This 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.
More information about this award is available at the SIGPLAN John C. Reynolds Dissertation Award Page.
The citation reads:
"This thesis proposes abstractions and formal tools to develop correct LLVM peephole optimizations. A domain specific language (DSL) Alive enables the specification and verification of peephole optimizations. An Alive transformation is shown to be correct automatically by encoding the transformation and correctness criteria as constraints in first-order logic, which are automatically checked for validity using an SMT solver. It then generates C++ code for an LLVM pass. Peephole optimizations in LLVM are executed numerous times until no optimization is applicable and one optimization could undo the effect of the other resulting in non-terminating compilation. A novel algorithm based on directed-acyclic-graph (DAG) composition determines whether such non-termination bugs can occur with a suite of peephole optimizations. The Alive toolkit can generate concrete input to demonstrate non-termination as well as automatically generating weakest preconditions. It is actively used by the LLVM community and has detected numerous bugs in existing passes and is preventing bugs from being added to the compiler."
David Menendez's project "Lightweight Formal Methods for LLVM Verification" under the supervision of Prof. Santosh Nagarakatte has had a good streak of high profile results:
PLDI 2015 Distinguished Paper Award for "Provably Correct Peephole Optimizations for Alive". Full paper here.
ICSE 2016 Distinguished Paper Award for "Termination-Checking for LLVM Peephole Optimizations". Full paper here.
ACM SIGPLAN Research Highlights Paper in October 2016. Citation here.
CACM Research Highlights Paper in February 2018. Full paper here.
Try out David's Alive-NJ tool kit that provides: (1) verification of both integer and floating point optimizations, (2) termination checking for a suite of peephole optimizations, and (3) automatic precondition inference for peephole optimizations.
Congratulations David Menendez on this prestigious honor!
Department of Computer Science