Congratulations to Professor Santosh Nagarakatte, his Ph.D. student David Menendez, their collaborators Nuno Lopez (MSR Cambridge) and Professor John Regehr (U. Utah) for winning the distinguished paper award at the ACM SIGPLAN 2015 Conference on Programming Language Design and Implementation (PLDI).
Their paper, “Provably Correct Peephole Optimizations with Alive,” considers the problem of proving LLVM peephole optimizations correct. To this end, it develops a domain-specific language, called Alive, in which compiler authors can express their optimization goals, and prove the correctness of the optimization using the help of an automated theorem prover. For a high-level overview of the research, see this entry on Prof. John Regehr’s blog: http://blog.regehr.org/archives/1170
PLDI is the premier forum for programming languages research, and is ACM’s flagship conference on the subject. This year, 58 papers were selected for publication at the conference, out of 303 submissions. Only 3 papers were selected as distinguished papers. These 3 papers will be presented in a special plenary session at the start of the conference, which will be held as part of the ACM Federated Computing Research Conferences (FCRC) in Portland, Oregon, in June 2015.