“Practical Verification of Peephole Optimizations with Alive”, a paper written by Rutgers CS professor Santosh Nagarakatte and a recent Rutgers CS PhD graduate David Menendez along with collaborators Nuno Lopes and John Regehr, has been published as a "Research Highlight" article in February 2018's Communications of the ACM (CACM) magazine.
The CACM Research Highlights (CACM-RH) section is devoted to the most important recent research results published in Computer Science. Papers in this section are first nominated by an editorial board or an ACM SIG selection committee, and then selected by a vote of the CACM-RH editorial board. A publication in CACM-RH provides unmatched visibility and is regarded as a significant honor.
The original Alive paper appeared in the the proceedings of PLDI 2015, where it was selected as the ACM SIGPLAN PLDI 2015 Distinguished Paper. This CACM Research Highlights article is a revised version of the PLDI 2015 paper to appeal to the broader CACM readership. The CACM article is preceeded by at "Technical Perspective" written by an expert in the field, in this case, Prof. Steve Zdancewic from University of Pennsylvania. In his perspective, Prof. Zdancewic states " .. [this project] takes a large step forward by showing how to build a tool that is practical yet backed by modern verification technology. In short, this paper suggests a way to make better compilers that are easier to build and far less buggy than they are today".
The CACM Research Highlight version of the work can be found here.
Prof. Steve Zdancewic's technical perspective on the paper can be found here.
David Menendez and Prof Santosh Nagarakatte's project on "Lightweight Formal Methods for LLVM Verification" 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
- Now, CACM Research Highlights Paper in February 2018
Try out David's Alive-NJ tool kit, which supports many extensions to Alive to verify floating point optimizations and automatic inference of preconditions.
Congratulations again, Prof. Santosh Nagarakatte and David Menendez!