Deriving Invariants by Algorithmic Learning, Decision Procedures, and Predicate Abstraction

Abstract

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

Short bio

Bow-Yaw Wang received his PhD degree from the department of computer and information science at University of Pennsylvania in 2001. Then he joined Verplex Systems, Inc in Silicon Valley and developed a functional property checker for hardware. He moved to Taiwan and worked in Academia Sinica since 2003.

Resources

• talk slide