Foundations of ILP-based Static Analysis

CCR-0306401基于ILP的静态分析的基础Jens Palsberg编译器是当今计算基础设施的重要组成部分，因为软件越来越多地使用高级编程语言编写。编译器的正确性通常是可取的，但对于传感器网络、医疗植入物和有线飞行/有线驾驶系统等嵌入式系统来说是绝对必要的。尽管在证明编译器正确性方面取得了实质性进展，但许多常用的编译器技术缺乏经过验证的基础。这个项目将关注基于整数线性规划(ILP)的静态分析的基础，ILP是嵌入式系统编译器常用的一种技术。本项目将研究基于ILP的分析的关键正确性属性，包括(1)可靠性：相对于形式语义，分析是否合理？(2)保存：程序转换后的分析是否保留？以及(3)组合：分析可以以保留程序基本属性的方式组合吗？有关基于ILP的分析正确性的基本结果将增加对生成代码的信心、开发新分析的原则、增加对如何组合分析的理解，以及基于ILP的代码认证，本着携带证明的代码、类型化汇编语言和Java字节码验证的精神。

CCR-0306401Foundations of ILP-based Static AnalysisJens PalsbergCompilers 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.