Title: Deriving Invariants by Algorithmic Learning, Decision Procedures, and Predicate Abstraction
Speaker:Dr. WANG Bow-Yaw £®Institute of Information Science, Academia Sinica, Taipei£©
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.