Automated Loop Invariant Generation For Program Verification

As the key method for ensuring correctness and improving reliability of software,verification receives more and more attentions. To play an irreplaceable role in verifi-cation, loop invariants are not only the basis of classical inductive assertion method forverifying properties of imperative programs, but also be more and more important to manymorden methods. Howerer, discovering invariants of loops automatically has been viewedas a considerable technical challenge.This thesis performs a systematic and deep study of the verification theories andalgorithms for discovering invariants of loops. Major contributions of this thesis are sum-marized into the following five aspects:1. We present a algorithm to generate polynomial equations as loop invariants. We alsoproof its correctness, give a condition for its termination. This algorithm remainssimple as algorithms that based on Gro¨bner bases computing and makes use of thestructure of path interleaving via control-?ow refinement for constructing strongerinvariants. It can generate disjunctive invariants.2. Based on Finite difference of expressions, we present a novel and simple approachto generating polynomial equations as loop invariants. we also proof the correctnessof this algorithm. This method relies on parameterized templates to solve nonlinearconstraints. Unlike related work, the generated constraints are linear equalities, whichcan be solved efficiently. Furthermore, invariants of higher degree can be constructedin terms of those of lower degree.3. We propose an QBF-based approach to construct invariants for program whose vari-ables are evaluated over finite domains. By employing parameterized templates, thismethod translates a program into constraints that are solved using a QBF (QuantifiedBoolean Formula) solver to yield desired program invariants. It supports non-linearexpressions that involving arbitrary bit-vector operations such as addition, multipli-cation, division, shift and bitwise operation, and can be used to discover a rich classof invariants including linear (or polynomial) equality (or inequality) invariants, andinvariants that contain quantifiers.4. We present a tool based on QBF. It bases on CIL and takes as input C source code, and can generate loop invariants automatically.5. We present a tool called CBOC to detect buffer over?ows in C source code. It baseson symbolic execution and introduces the notion of site-safe expression to optimizethe process of symbolic execution. CBOC bases on CIL and takes as input C sourcecode, and can identify buffer over?ows in the source code automatically.