Inferring Quantied Invariants via Algorithmic Learning, Decision Procedures, and Predicate Abstraction

By combining algorithmic learning, decision procedures, predicate abstraction, and simple templates, we present an automated technique for nding quantied loop invari- ants. Our technique can nd arbitrary rst-order invariants (modulo a xed set of atomic propositions and an underlying SMT solver) in the form of the given template and exploits the exibility in invariants by a simple randomized mechanism. The proposed technique is able to nd quantied invariants for loops from the Linux source, as well as for the benchmark code used in the previous works. Our contribution is a simpler technique than the previous works yet with the same derivation power.