View Full Document

12 views

Unformatted text preview:

SAT and Model Checking K L McMillan Cadence Berkeley Labs Outline Background Symbolic Model Checking DPLL style SAT solvers Bounded Model Checking SAT based model checking methods K induction Localization abstraction SAT based image computation Interpolation Copyright 2002 Cadence Design Systems Per Model checking Problem definition Does every run of a finite state transition system satisfy a given temporal property Result Yes No counterexample Examples Is every request to this bus arbiter eventually acknowledged Does this program every dereference a null pointer Copyright 2002 Cadence Design Systems Per Transition systems Tuple S I T where S is the finite set of states I S is the set of initial states T S S is the set of transitions A run of S I T is S where 0 I for all i 0 i i 1 T That is a run is an infinite path in the state graph strating with an initial state Copyright 2002 Cadence Design Systems Per Linear Temporal Logic LTL Augments propostitional logic with temporal operators Fp p is true some time in the future Gp p is true always in the future pUq eventually q until which p Xp p at next time Examples G req F gnt G req req U gnt G gnt req Copyright 2002 Cadence Design Systems Per Safety v Liveness Safety properties Bad thing never happens Characterized by bad finite prefixes an infinite run is bad exactly when it has a bad prefix Liveness properties Good thing eventually happens Pure liveness any finite behavior can be extended to a satisfying run We will concentrate only on safety properties but most results generalize to liveness Copyright 2002 Cadence Design Systems Per Reachability Problem def Does a transition system have a finite run ending in a state contained in the failure set F More precisely does there exist 0 k Sk s t 0 I and k F for all 0 i k i i 1 T Using automata theoretic methods model checking safety properties reduces to reachability analysis Given a t s M and a property P we can construct MP and FP such that M satisfies P exactly when FP



Access the best Study Guides, Lecture Notes and Practice Exams

Loading Unlocking...
Login

Join to view SAT and Model Checking and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view SAT and Model Checking and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?