Skip to content Skip to navigation

Lightweight Formal Methods for LLVM Verification and Intel MPX

Principal Investigator: 
Grant Agency: 
Intel Corporation
Grant Duration: 
08/01/2014 to 07/31/2019

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.