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

Speaker:Dr. WANG Bow-Yaw £®Institute of Information Science, Academia Sinica, Taipei£©

Time:3:30pm,Friday£¨March 26th

Venue:Lecture Room 334,State Key Lab of Computer Science, Level 3 Building #5, Institute of Software, CAS

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.