SAT and Model CheckingOutlineModel checkingTransition systemsLinear Temporal Logic (LTL)Safety v. LivenessReachabilityState explosion problemSymbolic transition systemsExampleSymbolic ReachabilitySymbolic reachability, cont.Expansion of quantifiersA two-bit counterRepresentationsDPLL-style SAT solversThe Implication Graph (BCP)Propositional ResolutionConflict ClausesConflict Clauses (cont.)Basic SAT algorithmGenerating refutationsCircuit SATBounded Model CheckingSymbolic Models (recall)Bounded model checkingBMC applicationsUnbounded Model CheckingK-inductionK-induction with a SAT solverSimple path assumptionInduction over simple paths...with a SAT solverTerminationLocalization abstractionConstraint granularityLocalization, contAlgorithmAbstract counterexamplesCounterexample extensionAbstraction refinementProof-based refinementIn other words...CCKSVW approach (FMCAD02)CCKSVW approach cont.Weakness of Cex-based approachProof-based abstractionBMC phaseAbstraction phaseSlide 50Slide 51Weakness of proof-based absPicoJavaII benchmarksAbstraction resultsInferenceComparing CBA and PBARun time comparisonAbstraction comparisonPossible explanationPBA run-time breakdownCBA run-time breakdownIBM GP benchmarksCompare to K-induction on PicoJavaA (fuzzy) hypothesisIndustrial benchmarksImplicationsImage computation methodsSymbolic model checkingSyntactic expansion of quantifiersLimitationsDirect image computationCircuit ValidityCNF CharacterizationBlocking clausesAn exampleAlternate implication graphBlocking clause exampleCNF characterization algorithmUniversal Quantifier Elimination" - elimination algorithmCTL Model Checking with SATRecent related workSimplified PicoJavaII benchmarksComparison with BDD’sSAT-based imageImage over-approximationInterpolationInterpolation-based MCSlide 89OverapproximationAdequate imagek-adequate image operatorInterpolation-based imageHuh?IntuitionReachability algorithmSlide 97PicoJava II Benchmarksvs. k-inductionSlide 100GP benchmarks - true propertiesSlide 102ConclusionConclusion cont.SAT and Model CheckingK. L. McMillanCadence Berkeley LabsCopyright 2002 Cadence Design Systems. Permission is granted to reproduce without modification.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–InterpolationCopyright 2002 Cadence Design Systems. Permission is granted to reproduce without modification.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. Permission is granted to reproduce without modification.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 stateCopyright 2002 Cadence Design Systems. Permission is granted to reproduce without modification.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. Permission is granted to reproduce without modification.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 livenessCopyright 2002 Cadence Design Systems. Permission is granted to reproduce without modification.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 is not reachable in MP.Copyright 2002 Cadence Design Systems. Permission is granted to reproduce without modification.State explosion problem•Reachability analysis can be done by BFS or DFS on the state graph.•However, |S| is exponential in system size–for example 2n, where n is number of registers•Impractical to construct the state graph explicitly.Our topic is essentially how to use a SAT solver to tackle this problem.Copyright 2002 Cadence Design Systems. Permission is granted to reproduce without modification.Symbolic transition systems•Tuple (S,I,T), where:–S is a signature,–I is a formula over S (the initial condition)–T is a formula over SS' (the transition condition)•States:  = S{0,1}•A run of (S,I,T) is , where:–I[0]–for all i  0, T[i ,i+1]Note: T[i ,i+1] means T[i 'i+1]Copyright 2002 Cadence Design Systems. Permission is granted to reproduce without modification.ExampleT is a conjunction of constraits, one per component.abcpgg = a  bp = g  cc' = pT = { g = a  b, p = g  c, c' = p }Copyright 2002 Cadence Design Systems. Permission is granted to reproduce without modification.Symbolic ReachabilityI FR1R2...R= I  Img(I,C)= R1  Img(R1,C)Idea: represent reachable states by a formulaEssentially a BFS with symbolic representation.Copyright 2002 Cadence Design Systems. Permission is granted to reproduce without modification.Symbolic reachability, cont.•Reachability fixed point:R0 = IRi+1 = Ri  Img(Ri,T)R =  Ri•F is reachable iff R  F  false•Image operator:Img(P,T) = S'.  S. (P(V)  T(V,V’))We need a way to eliminate the quantifier, to get us back to an ordinary Boolean formula.Copyright 2002 Cadence Design Systems. Permission is granted to reproduce without modification.Expansion