Affine Loop Invariant Generation via Matrix Algebra

Loop invariant generation, which automates the generation ofassertions that always hold at the entry of a while loop, has many importantapplications in program analysis and formal verification. In this work, wetarget an important category of while loops, namely affine while loops, thatare unnested while loops with affine loop guards and variable updates. Sucha class of loops widely exists in many programs yet still lacks a general butefficient approach to invariant generation. We propose a novel matrix-algebraapproach to automatically synthesizing affine inductive invariants in theform of an affine inequality. The main novelty of our approach is that (i)the approach is general in the sense that it theoretically addresses all thecases of affine invariant generation over an affine while loop, and (ii) it canbe efficiently automated through matrix-algebra (such as eigenvalue, matrixinverse) methods.The details of our approach are as follows. First, for the case where the loopguard is a tautology (i.e., ‘true’), we show that the eigenvalues and theireigenvectors of the matrices derived from the variable updates of the loopbody encompass all meaningful affine inductive invariants. Second, for themore general case where the loop guard is a conjunction of affine inequalities,our approach completely addresses the invariant-generation problem by firstestablishing through matrix inverse the relationship between the invariantsand a key parameter in the application of Farkas’ lemma, then solving thefeasible domain of the key parameter from the inductive conditions, andfinally illustrating that a finite number of values suffices for the key parameterw.r.t a tightness condition for the invariants to be generated.Experimental results show that compared with previous approaches, ourapproach generates much more accurate affine inductive invariants overaffine while loops from existing and new benchmarks within a few seconds,demonstrating the generality and efficiency of our approach