Seminar talk by Dr. Santosh Nagarkatte

On 10th August 2016, Dr. Santosh Nagarakatte delivered a talk on Lightweight Formal Methods for LLVM Verification. Dr. Nagarakatte, an Assistant Professor at Rutgers University, primarily conducts research in hardware-software interfaces spanning programming languages, compilers, runtimes, and computer architecture.
Dr. Nagarakatte introduced the LLVM compiler and spoke at length about its salient features. He explained the catastrophic effects that incomplete test harnesses might have on real world code. He drew an analogy between bugs in compilers and weak links of otherwise strong chains, highlighting the delicate balance between formal methods and usability. He also talked about how compilers could lead to bugs in the code during the process of optimization. He introduced Alive, a fast and easy DSL for instCombine optimizations.

Dr. Nagarakatte had a dynamic discussion with the audience. He ended the interactive talk with a description of several ongoing projects that are pushing the limits in this area.