Compilers are an important part of today's computational infrastructure as software is ever-increasingly written in high-level programming languages. Compiler correctness is generally desirable but absolutely essential for embedded systems like sensor networks, medical implants, and fly-by-wire/drive-by-wire systems. Many commonly used compiler techniques lack proven foundations despite substantial advances in the field of proving compiler correctness. This project will focus on the foundations of static analysis based on integer linear programming (ILP), a technique commonly used by compilers for embedded systems. This project will investigate key correctness properties of ILP-based analyses, including (1) soundness: is the analysis sound with respect to a formal semantics? (2) preservation: is the analysis preserved after program transformations? and (3) composition: can analyses be combined in ways that preserve basic properties of the program? Foundational results about the correctness of ILP-based analyses will lead to increased confidence in generated code, principles for developing new analyses, increased understanding of how to combine analyses, and ILP-based code certification, in the spirit of proof-carrying code, typed assembly language, and Java bytecode verification.
