• Santosh Nagarakatte
  • Abstract:

    Compilers are crucial components of the computing ecosystem. They can transform source programs written in multiple languages (e.g, C/C++/Java) into multiple target architectures (e.g, x86/ARM). Compiler bugs, however, break properties enforced at the level of source programs and can lead to unintended application behavior and disasters in safety-critical domains. This project aims to develop pragmatic and lightweight formal techniques for making mainstream compilers robust, in a manner that can be easily adopted by compiler developers. The intellectual merit of this project is the development of real-world compiler verification environments drawing influence from multiple areas like programming languages, architecture, and concurrency. The project's broader significance and importance are: (1) improving the quality of a large number of software projects by improving the robustness of the compiler, (2) inculcating formal reasoning for building large systems (compilers in particular) that are correct by construction, and (3) educating high school students, undergraduates, and graduate students for developing software with lightweight formal methods.

    This project aims to build new techniques and tools that can check the correctness of optimizations with the help of the developer. The project achieves this by (1) designing mathematically-precise semantics for various components of the mainstream LLVM compiler, (2) designing domain specific languages for writing and specifying LLVM optimizations, which not only check optimizations for correctness but also generate efficient C++ implementations, (3) designing techniques to build precise translation validators, which compare the source and the target code with assistance from the compiler developer. Technology developed by this research will not only improve the reliability of compilers but also the reliability of other large software systems which depend on correct compilation.

  • Grant Title: CAREER: Semantics, Abstractions, and Tools for a Pragmatic Verified LLVM Compiler
  • Principal Investigator:: Santosh Nagarakatte
  • Grant Agency: National Science Foundation
  • Grant Duration: 01/15/2015 to 12/31/2019
  • Amount: $545,000

Congratulations to Prof. Santosh Nagarakatte, who has just been awarded the prestigious NSF CAREER award for his project entitled “CAREER: Semantics, Abstractions, and Tools for a Pragmatic Verified LLVM Compiler.” The grant runs for a period of 5 years, from 2015 to 2019, and is for an amount of $545,000

The main aim of the project is to develop tools to assist compiler writers to build compilers that are correct by construction. Compilers are complex pieces of software, and prior research has shown that even mature compilers have subtle bugs in them that can manifest themselves in various ways in the applications that they are used to compile. Santosh’s CAREER award proposes a research, education and outreach plan that will develop lightweight formal methods to assist in the creation of verified compilers, particularly targeting the popular, open-source LLVM compiler. For a flavor of the work proposed in Santosh’s project, check out the following blog post on the ALIVE (Automatic LLVM InstCombine Verifier) project: http://blog.regehr.org/archives/1170

For more details on Santosh’s CAREER grant, please consult NSF’s website: http://www.nsf.gov/awardsearch/showAward?AWD_ID=1453086 To quote the NSF, “The Faculty Early Career Development (CAREER) Program is a Foundation-wide activity that offers the National Science Foundation’s most prestigious awards in support of junior faculty who exemplify the role of teacher-scholars through outstanding research, excellent education and the integration of education and research within the context of the mission of their organizations. Such activities should build a firm foundation for a lifetime of leadership in integrating education and research.”