Automatically inferring loop invariants via algorithmic learning

摘要

By combining algorithmic learning, decision procedures, predicate abstraction and simplerntemplates for quantified formulae, we present an automated technique for finding looprninvariants. Theoretically, this technique can find arbitrary first-order invariants (modulo arnfixed set of atomic propositions and an underlying satisfiability modulo theories solver) inrnthe form of the given template and exploit the flexibility in invariants by a simplernrandomized mechanism. In our study, the proposed technique was able to find quantifiedrninvariants for loops from the Linux source and other realistic programs. Our contribution isrna simpler technique than the previous works yet with a reasonable derivation power.