News

Left Square Image
Referenced People:
  • Nagarakatte, Santosh
  • Abstract:

    Compilers form an integral component of the software development ecosystem. Compiler writers must understand the specification of source and target languages to design sophisticated algorithms that transform programs while preserving semantics. Unfortunately, compiler bugs in industrial strength compilers are common. Compiler bugs can manifest as crashes during compilation, or, much worse, result in the silent generation of incorrect programs. Such mis-compilations can introduce subtle errors that are difficult to diagnose and generally puzzling to software developers. Verification of compiler implementations with automation can not only eliminate compiler bugs but also make it practical to build robust compilers.

    This proposal has three broad directions toward the goal of building a robust verified LLVM compiler: (1) formalize the semantics of various components of the LLVM compiler for both sequential and concurrent settings, (2) develop an environment based on first-order logic, decision procedures, tools, and techniques to automate the process of verifying compiler optimizations, and (3) develop a domain specific language to enable the optimization writer to assist the generation of verified optimizations. An important goal is to automate the process of building verified compilers leveraging SMT (satisfiability modulo theories) solvers while minimizing the need for interactive proofs. 

    Grant Title: Semi-automated Verification of LLVM Optimizations with SMT Solvers
    Principal Investigator:: Santosh Nagarakatte
    Grant Agency: Google
    Grant Duration: 02/15/2014 to 12/31/2019
    Amount: $63,500

    Congratulations to Prof. Santosh Nagarakatte, who has just received a Google Faculty Research Award. He was awarded an amount of $63500 for his project entitled “Semi-Automated Verification of LLVM Optimizations using SMT Solvers”. This project addresses the goal of of building a robust verified LLVM compiler by (1) formalizing the semantics of various components of the LLVM compiler and (2) developing tools and techniques to automate the process of verifying compiler optimizations leveraging SMT (satisfiability modulo theories) solvers while minimizing the need for interactive proofs.