News

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

    Compilers  form an integral component of the software development ecosystem. Unfortunately, compiler bugs in mainstream compilers are common, which manifest either as crashes during compilation, or, much worse, result in the silent generation of incorrect programs. This award supports research  to develop tools and techniques to prove the correctness of the specification of optimizations in the LLVM compiler and to generate C++ implementations from the specification.  The award also supports the exploration of a LLVM target for Intel Memory Protection Extensions.

    Grant Title: Lightweight Formal Methods for LLVM Verification and Intel MPX
    Principal Investigator:: Santosh Nagarakatte
    Grant Agency: Intel Corporation
    Grant Duration: 08/01/2014 to 07/31/2019
    Amount: $145,000

    Congratulations to Prof. Santosh Nagarakatte, who has just received a research grant from Intel Corp. The grant, for an amount of $75000, funds his research in the area of “Lightweight Formal Methods for LLVM Verification and a MPX target for LLVM.” Compilers form an integral component of the software development ecosystem. Unfortunately, compiler bugs in mainstream compilers are common, which manifest either as crashes during compilation, or, much worse, result in the silent generation of incorrect programs. This award supports research to develop tools and techniques to prove the correctness of the specification of optimizations in the LLVM compiler and to generate C++ implementations from the specification. The award also supports the exploration of a LLVM target for Intel Memory Protection Extensions.