Safety Model Checking with Complementary Approximations Jianwen Li, Shufang Zhu, Yueling Zhang, Geguang Pu, Moshe Y. Vardi Presented by Marek Chalupa IA072 – spring 2021, March 12, 2021 Complementary Approximate Reachability (CAR) Technique for verifying invariant properties of boolean transition systems. Inspired by symbolic reachability and IC3/PDR Aims to find a property violation as fast as possible Works complementary to IC3/PDR ·CAR ·IA072 – spring 2021, March 12, 2021 2 / 12 Preliminaries We use propositional logic (boolean variables, connectives ∧, ∨, ¬, =⇒ , ⇐⇒ ). A variable or its negation is called literal, conjunction of literals is cube and disjunction of literals is clause. ·CAR ·IA072 – spring 2021, March 12, 2021 3 / 12 Preliminaries We use propositional logic (boolean variables, connectives ∧, ∨, ¬, =⇒ , ⇐⇒ ). A variable or its negation is called literal, conjunction of literals is cube and disjunction of literals is clause. A formula over variables X = {x1, . . . , xn} is satisfiable (SAT) if there exists an assignment α : X → {true, false} to its variables that evaluates the formula to true. We allow α to be partial function, in which case we call the assignment partial assignment. ·CAR ·IA072 – spring 2021, March 12, 2021 3 / 12 Preliminaries We use propositional logic (boolean variables, connectives ∧, ∨, ¬, =⇒ , ⇐⇒ ). A variable or its negation is called literal, conjunction of literals is cube and disjunction of literals is clause. A formula over variables X = {x1, . . . , xn} is satisfiable (SAT) if there exists an assignment α : X → {true, false} to its variables that evaluates the formula to true. We allow α to be partial function, in which case we call the assignment partial assignment. If a formula φ is unsatisfiable (UNSAT), we can find its minimal unsat core (MUC) which is a subformula ψ of φ which is UNSAT but every subformula of ψ is SAT. ·CAR ·IA072 – spring 2021, March 12, 2021 3 / 12 Preliminaries – cont. Boolean transition system (BTS) is a tuple (¯x, I, T) consisting of state (boolean) variables ¯x = {x1, x2, ..., xn}, a propositional formula I(¯x) describing initial states, a propositional formula T(¯x, ¯x ) describing transition relation Where ¯x are the next-state versions of state variables: {x1, x2, ..., xn}. ·CAR ·IA072 – spring 2021, March 12, 2021 4 / 12 Preliminaries – cont. Boolean transition system (BTS) is a tuple (¯x, I, T) consisting of state (boolean) variables ¯x = {x1, x2, ..., xn}, a propositional formula I(¯x) describing initial states, a propositional formula T(¯x, ¯x ) describing transition relation Where ¯x are the next-state versions of state variables: {x1, x2, ..., xn}. A predicate over ¯x represents a set of states. Notably, a conjunction of n (different) literals represents a single state. ·CAR ·IA072 – spring 2021, March 12, 2021 4 / 12 BTS Example 000 111 100 010 001 110 011 101 ¯x = {x1, x2, x3} I(¯x) = ¬x2 ∧ ¬x3 T(¯x, ¯x ) = (x1 ⇐⇒ x2) ∧ (x2 ⇐⇒ x3) ∧ (x3 ⇐⇒ x1) P(¯x) = ¬x1 ∨ ¬x2 ·CAR ·IA072 – spring 2021, March 12, 2021 5 / 12 Preliminaries – cont. From now on, we fix some BTS (¯x, I, T) and a set of states P called property. Notation: we do not write arguments to named formulas. That is, we abbreviate I(¯x) to I and T(¯x, ¯x ) to T. Formula F is the formula F with all variables primed. E.g., if F = x ∧ y then F = x ∧ y . If F = z ∧ y , then F = z ∧ y , etc. ·CAR ·IA072 – spring 2021, March 12, 2021 6 / 12 Preliminaries – cont. From now on, we fix some BTS (¯x, I, T) and a set of states P called property. Notation: we do not write arguments to named formulas. That is, we abbreviate I(¯x) to I and T(¯x, ¯x ) to T. Formula F is the formula F with all variables primed. E.g., if F = x ∧ y then F = x ∧ y . If F = z ∧ y , then F = z ∧ y , etc. A set of states is invariant of BTS if it is a superset of reachable states. A set S of states is inductive (closed under reachability) if I =⇒ S S ∧ T =⇒ S ·CAR ·IA072 – spring 2021, March 12, 2021 6 / 12 Model Checking of BTSs Assume we want to show that all states reachable from I satisfy a predicate P. The basic option is to enumerate states reachable in 0, 1, 2, ... steps. ·CAR ·IA072 – spring 2021, March 12, 2021 7 / 12 Model Checking of BTSs Assume we want to show that all states reachable from I satisfy a predicate P. The basic option is to enumerate states reachable in 0, 1, 2, ... steps. But that is not efficient for large systems. ·CAR ·IA072 – spring 2021, March 12, 2021 7 / 12 Model Checking of BTSs Assume we want to show that all states reachable from I satisfy a predicate P. The basic option is to enumerate states reachable in 0, 1, 2, ... steps. But that is not efficient for large systems. Another option is to try to find an inductive invariant F such that F =⇒ P, i.e., I =⇒ F F ∧ T =⇒ F F =⇒ P ·CAR ·IA072 – spring 2021, March 12, 2021 7 / 12 Model Checking of BTSs – cont. A useful technique for finding inductive invariants for BTSs is IC3/PDR: IC3/PDR maintains an over-approximation F of states reachable in at most k steps (k is being increased if found insufficient) it iteratively blocks states that fail the inductiveness of F until F becomes inductive or a counter-example (real error) is found. IC3/PDR generalizes the blocked states to speed-up the convergence to an invariant. Problem 1: the generalization has a big over-head. Problem 2: it may take a long time to find a counter-example. ·CAR ·IA072 – spring 2021, March 12, 2021 8 / 12 Model Checking of BTSs – cont. CAR is inspired by IC3/PDR but tries to solve: Problem 1 (the generalization in IC3/PDR has a big over-head) by using MUC for the generalization. MUC are provided virtually free by SAT solvers. Problem 2 (it may take a long time to find a counter-example) by using also an under-approximation of states that reach bad states. ·CAR ·IA072 – spring 2021, March 12, 2021 9 / 12 CAR Algorithm (main loop) assume Bi , Fi = false, true for all i > 0 F0, B0 ← I, ¬P # check the first two steps from init if sat(F0 ∧ B0) or sat(F0 ∧ T ∧ B0): return unsafe (+ cex) for i in 1, 2, . . . : Fi ← P cex ← strengthen # a counter-example (real error) found if cex: return unsafe (+ cex) # some frame got inductive if ∃j ≤ i : Fj =⇒ m