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.