Skip to content Skip to navigation

Pragmatic Abstractions, Techniques, and Tools for LLVM Verification

Principal Investigator: 
Grant Agency: 
Intel Corporation
Grant Duration: 
11/02/2016 to 11/02/2021

This unrestricted gift funds Prof. Santosh Nagarakatte's research on LLVM verification. Prof. Nagarakatte's research group is designing lightweight formal tools that enable compiler writers to develop correct peephole optimizations for LLVM, a widely used mainstream compiler. This award supports further enhancements to the Alive-NJ prototype to reason about the correctness of floating point optimizations, to assist compiler writers when optimizations are not correct, and to extend the class of optimizations handled by Alive-NJ.