Ph.D. student in Computer Science at Rutgers University.email@example.com
My research focuses on applying light-weight formal methods to software verification, especially compiler correctness. I work with Professor Santosh Nagarakatte in the RAPL group.
David Menendez and Santosh Nagarakatte. “Alive-Infer: Data-Driven Precondition Inference for Peephole Optimizations in LLVM” In Proceedings of the 38th Annual ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI, June 2017. [DOI, Video]
David Menendez, Santosh Nagarakatte, and Aarti Gupta. “Alive-FP: Automated verification of floating point based peephole optimizations in LLVM” In Proceedings of the 23rd International Static Analysis Symposium, SAS, Aug. 2016.
David Menendez and Santosh Nagarakatte.
“Termination checking for LLVM peephole optimizations”
In Proceedings of the 38th International Conference for Software Engineering,
ICSE, May 2016.
ACM SIGSOFT Distinguished Paper Award
Nuno Lopes, David Menendez, Santosh Nagarakatte, and John Regehr.
“Provably correct peephole optimizations with Alive”
In Proceedings of the 36th Annual ACM SIGPLAN Conference on Programming Language Design and Implementation,
ACM SIGPLAN Distinguished Paper Award
SIGPLAN Research Highlight
CACM Research Highlight
Alive (Automated LLVM's InstCombine Verifier).
A language for specifying optimizations for LLVM's InstCombine pass. Our tool can automatically checking the correctness of optimizations specified in Alive, and can generate C++ code which implements the optimization.
An extension of Alive which checks whether a sequence of optimizations can be performed indefinitely on a finite input program (e.g., if one optimization undoes another) and tests whether such examples exist in a set of Alive optimizations.
A re-implementation of Alive designed for improved extensibility. Implements the floating-point semantics described by Alive-FP and includes the precondition inference described by Alive-Infer.