News

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.