Generating Octagonal Invariants using Quantifier Elimination Heuristics

随着软件变得越来越复杂，在缺乏完整的正式和严格的规范的情况下，确保其完全正确性已经成为一项非常重要的任务。轻量级程序分析技术，超越类型检查和检测语义错误，因此变得越来越相关。特别是考虑到诸如缓冲区溢出之类的错误可以被利用来造成严重破坏，使组织陷入停滞并造成相当大的财务损失。这个项目将探索几何算法的量词消除，自动推导出一类有限的不变性质的程序，与发展可扩展的高效算法的程序分析的目标。将特别注意使用数值关系约束程序变量表示的属性;工业经验表明，从未注释和未指定的程序中自动导出这些属性对于查找工业软件中的错误非常有用。最近取得的进展，可满足性模理论（SMT）求解器和自动推理技术，以及已经建成的工具，量词消除将被利用来实现这一目标。这个项目将建立一个技术库，用于分析程序的工具，包括优化编译器，调试器和验证器，以及用于识别计算机网络中的安全违规行为。

With software becoming more and more complex, ensuring its total correctness, in the absence of full formal and rigorous specifications, has become a highly nontrivial task. Lightweight program analysis techniques which go beyond type checking and detect semantic bugs are thus becoming increasing relevant. This is especially so given that bugs such as buffer overflows can be exploited to cause havoc, bringing organizations to a stand-still and causing considerable financial loss. This project will explore geometric heuristics for quantifier elimination to automatically derive a restricted class of invariant properties of programs, with the goal of developing scalable highly efficient algorithms for program analysis. Particular attention will be paid to properties expressed using numerical relational constraints on program variables; industrial experience suggests that automatically deriving such properties from unannotated and unspecified programs is extremely useful in finding bugs in industrial software. Recent advances made in satisfiability modulo theories (SMT) solvers and automated reasoning techniques as well as already built tools for quantifier elimination will be exploited to achieve this. This project will build a repertoire of techniques to be used in tools analyzing programs including optimizing compilers, debuggers, and verifiers as well as those for identifying security violations in computer networks.