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

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.