SAT and Model Checking - University of Toronto

SAT and Model Checking - University of Toronto

SAT and Model Checking Bounded Model Checking (BMC) Biere, Cimatti, Clarke, Zhu, 1999 A.I. Planning problems: can we reach a desired state in k steps? Verification of safety properties: can we find a bad state in k steps? Verification: can we find a counterexample in k steps ? What is SAT?

Given a propositional formula in CNF, find if there exists an assignment to Boolean variables :that makes the formula true literals clauses 11==(bb (bb c) c) 22==(b(baa d) d) 33==(b(bbb d) d) ==11 22 33 AA=={a=0, {a=0,b=1,

b=1,c=0, c=0,d=1} d=1} SATisfying assignment! BMC idea Given: transition system M, temporal logic formula f, and user-supplied time bound k Construct propositional formula (k) that is satisfiable iff f is valid along a path of length k Path of length k: I ( s0 ) k1

i0 R( si , si1 ) Say f = EF p and k = 2, then (2) I ( s0 ) R( s0 , s1 ) R( s1 , s2 ) ( p0 p1 p2 ) What if f = AG p ? BMC idea (contd) AG p means p must hold in every state along any path of length k We take (k ) ( I ( s0 ) So (k ) I ( s0 )

k1 k i0 R( si , si1 )) i0 pi k1 k i0 R( si , si1 ) i0 pi That means we look for counterexamples Safety-checking as BMC p is preserved up to k-th transition iff (k) is unsatisfiable: (k ) I ( s0 )

k1 k i0 R(si , si1 ) i0 p p p p s0 s1 s2

... p sk-1 p sk If satisfiable, satisfying assignment gives counterexample to the safety property. Example: a two bit counter Initial state: I : l r 00

11 01 10 l ' (l r ) Transition: R : r ' r Safety property: AG ( l r ) (l 0 r0 ) l1 (l 0 r0 ) r1 r0 (l1 r1 ) (2) : ( l 0 r0 ) l 2 (l1 r1 ) r2 r1 (l r ) 2 2

(2) is unsatisfiable. (3) is satisfiable. Example: another counter 00 11 01 10 l ' l

l ' (l r ) I : l r R: r ' r r ' r l r Liveness property: AF (l r ) Check: EG ( l r )

(2) I ( s0 ) where 1 2 i0 R( si , si1 ) i0( li ri ) loop loop R( s2 , s3 ) ( s3 s0 s3 s1 s3 s2 ) (2) is satisfiable Satisfying assignment gives counterexample to the liveness property What BMC with SAT Can Do All LTL

ACTL and ECTL In principle, all CTL and even mu-calculus efficient universal quantifier elimination or fixpoint computation is an active area of research How big should k be? For every model M and LTL property there exists k s.t. The minimal such k is the Completeness Threshold (CT) How big should k be? Diameter d = longest shortest path from an initial state to any other reachable state. Recurrence Diameter rd = longest loop-free path.

rd d d=2 rd = 3 How big should k be? Theorem: for Gp properties CT = d p s0 Arbitrary path How big should k be? Theorem: for Fp properties CT= rd p p

p p p s0 Open Problem: The value of CT for general Linear Temporal Logic properties is unknown A basic SAT solver Given in CNF: (x,y,z),(-x,y),(-y,z),(-x,-y,-z) Decide() X

X X Deduce() X X Resolve_Conflict() Basic Algorithm Choose the next variable and value. Return False if all variables are assigned

While (true) { if (!Decide()) return (SAT); while (!Deduce()) if (!Resolve_Conflict()) return (UNSAT); } Apply unit clause rule. Return False if reached a conflict Backtrack until no conflict. Return False if impossible DPLL-style SAT solvers

SATO,GRASP,CHAFF,BERKMIN A= empty clause? y UNSAT n Obtain conflict clause and backtrack Branch: add some literal to A

y conflict? n is A total? y SAT The Implication Graph (a b) (b c d) a c b

d Decisions Assignment: a b c d Resolution a b c a c d b c d When a conflict occurs, the implication graph is used to guide the resolution of clauses, so that the same conflict will not occur again. Conflict clauses (a b) (b c d) (b d)

resolve a c (b c ) b Conflict! Conflict! (a c) d resolve Conflict! Decisions Assignment: a b c d

Conflict Clauses (cont.) Conflict clauses: Are generated by resolution Are implied by existing clauses Are in conflict with the current assignment Are safely added to the clause set Many heuristics are available for determining when to terminate the resolution process. Generating refutations Refutation = a proof of the null clause Record a DAG containing all resolution steps performed during conflict clause generation. When null clause is generated, we can extract a proof of the null clause as a resolution DAG.

Original clauses Derived clauses Null clause Unbounded Model Checking A variety of methods to exploit SAT and BMC for unbounded model checking: Completeness Threshold k - induction Abstraction (refutation proofs useful here) Exact and over-approximate image computations (refutation proofs useful here) Use of Craig interpolation

Conclusions: BDDs vs. SAT Many models that cannot be solved by BDD symbolic model checkers, can be solved with an optimized SAT Bounded Model Checker. The reverse is true as well. BMC with SAT is faster at finding shallow errors and giving short counterexamples. BDD-based procedures are better at proving absence of errors. Acknowledgements Exploiting SAT Solvers in Unbounded Model Checking by K. McMillan, tutorial presented at CAV03 Tuning SAT-checkers for Bounded Model Checking and Heuristics for Efficient SAT solving by O. Strichman Slides originally prepared for 2108 by Mihaela Gheorghiu.

Recently Viewed Presentations

  • America's First Government(s) - Cabarrus County Schools

    America's First Government(s) - Cabarrus County Schools

    The first constitution of the US. Proposed by the Continental Congress November 17, 1777. Ratified by all the states on March 1, 1781. The . Confederation. created a "league of friendship" coming together for one purpose. ... America's First Government(s)
  • Expanded PrEP implementation across Australia Expanded implementation of

    Expanded PrEP implementation across Australia Expanded implementation of

    The 2014 HIV diagnosis and care cascade. Source: State and Territory health authorities, Australia. Number of people Living with HIV Diagnosed with HIV Receiving treatment Suppressed virus 27150 23800 17470 16090 Expanded PrEP implementation across Australia
  • Economic Benefits of Rare and Endangered Species

    Economic Benefits of Rare and Endangered Species

    Economic Benefits of Rare and Endangered Species Loomis, J.B., White, D.S. "Economic Benefits of Rare and Endangered Species: Summary and Meta-Analysis." Ecological Economics 18(1996): 197-206. Lauren Goschke Questions #1- What kinds of economic costs and benefits are provided by Threatened...
  • ECE408 / CS483 Applied Parallel Programming Lecture 18:

    ECE408 / CS483 Applied Parallel Programming Lecture 18:

    © David Kirk/NVIDIA and Wen-mei W. Hwu, 2007-2012 ECE408/CS483, University of Illinois, Urbana-Champaign. Examples of Paradigm Shift. 20th Century
  • MIH Molar Incisor Hypomineralization

    MIH Molar Incisor Hypomineralization

    Compomer. RBC . Glass ionomers and resin-modified glass ionomers have poor wear resistance and are not recommended for placement in stress-bearing areas . The enamel-adhesive interface. Porous . Cracks. Decreased bond strength. Cohesive failure
  • Research Methods for the Learning Sciences

    Research Methods for the Learning Sciences

    Penalize models with more clusters, according to how much extra fit would be expected from the additional clusters. Our old friend the Bayesian Information Criterion. Not just the same as cross-validation for this problem!
  • Maternal physiology during pregnancy

    Maternal physiology during pregnancy

    Production of thyroid hormone increases by 40% to 100% to meet maternal and fetal demands. The thyroid gland undergoes moderate enlargement during pregnancy . Circulating thyroid hormone exists in two primary active forms: thyroxine (T4) and triiodothyronine (T3).
  • LO4 Capital Cost Allowance (CCA)  CCA is depreciation

    LO4 Capital Cost Allowance (CCA) CCA is depreciation

    Capital Cost Allowance (CCA) LO4 CCA is depreciation for tax purposes The depreciation expense used for capital budgeting should be calculated according to the CCA schedule dictated by the tax code Depreciation itself is a non-cash expense, consequently, it is...