Generating Octagonal Invariants using Quantifier Elimination Heuristics

University Of New Mexico, Albuquerque NM

Investigators

Abstract

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.