K.: Deriving invariants by algorithmic learning, decision procedures, and predicate abstraction. Technical Memorandum ROSAEC-2009-004, Research On Software Analysis for Error-Free Computing

Abstract. By combining algorithmic learning, decision procedures, and predicate abstraction, we present an automated technique for finding loop invariants in propositional formulae. Given invariant approxima-tions derived from pre- and post-conditions, our new technique exploits the flexibility in invariants by a simple randomized mechanism. The pro-posed technique is able to generate invariants for some Linux device drivers and SPEC2000 benchmarks in our experiments.