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.