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

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.