Interpolating Strong Induction Hari Govind Vediramana Krishnan, Yakir Vizel, Vijay Ganesh, Arie Gurfinkel Presented by Marek Chalupa IA072 – spring 2021, May 21, 2021 The algorithm KAVY Technique for safety verification of symbolic transition systems. Combines: IC3/PDR (bounded model checking with) iterpolation k-induction (AVY ∼ PDR-like algorithm with interpolation) Strong induction = k-induction „KAVY uses k-induction to guide interpolation and PDR-style inductive generalization” ·KAVY ·IA072 – spring 2021, May 21, 2021 2 / 15 Symbolic transition systems Symbolic transition system 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 ·KAVY ·IA072 – spring 2021, May 21, 2021 3 / 15 Symbolic transition systems Symbolic transition system 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 Safety verification: given a set of good states P (the property), we want to decide whether all reachable states of the system are in P (P-states). If yes, we call the system safe (unsafe otherwise). ¬P-states are called bad states. ·KAVY ·IA072 – spring 2021, May 21, 2021 3 / 15 Symbolic transition system 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 ·KAVY ·IA072 – spring 2021, May 21, 2021 4 / 15 Inductive sets Given a system (x, I, T), a set S of states is inductive invariant if I(x) =⇒ S(x) S(x) ∧ T(x, x ) =⇒ S(x ) ·KAVY ·IA072 – spring 2021, May 21, 2021 5 / 15 Inductive sets Given a system (x, I, T), a set S of states is inductive invariant if I(x) =⇒ S(x) S(x) ∧ T(x, x ) =⇒ S(x ) A set S of states is k-inductive invariant if I(x0) ∧ T(x0, x1) ∧ · · · ∧ T(xk−2, xk−1) =⇒ 0≤i≤k−1 S(xi ) S(x0) ∧ T(x0, x1) ∧ S(x1) ∧ T(x1, x2) ∧ · · · ∧ S(xk−1) ∧ T(xk−1, xk) =⇒ S(xk) ·KAVY ·IA072 – spring 2021, May 21, 2021 5 / 15 Bounded model checking (BMC) Given a parameter k, we check the formula: I(x0) ∧ T(x0, x1) ∧ . . . T(xk−1, xk) ∧ (¬P(x0) ∨ · · · ∨ ¬P(xk)) ·KAVY ·IA072 – spring 2021, May 21, 2021 6 / 15 Bounded model checking (BMC) Incremental BMC: for parameter k = 0, 1, 2, ..., we check the formula: I(x0) ∧ T(x0, x1) ∧ . . . T(xk−1, xk) ∧ ¬P(xk) ·KAVY ·IA072 – spring 2021, May 21, 2021 6 / 15 Bounded model checking with k-induction For parameter k = 0, 1, 2, ..., we check the formulas: base: I(x0) ∧ T(x0, x1) ∧ . . . T(xk−1, xk) ∧ ¬P(xk) step: P(x0) ∧ T(x0, x1) ∧ . . . T(xk−1, xk) ∧ P(xk) ∧ T(xk, xk+1) ∧ ¬P(xk+1) ·KAVY ·IA072 – spring 2021, May 21, 2021 7 / 15 Interpolants Given two formulas A, B such that A ∧ B is unsat, a Craig’s interpolant is a formula R, such that: A =⇒ R R ∧ B is unsat R uses only variables common to A and B ·KAVY ·IA072 – spring 2021, May 21, 2021 8 / 15 BMC with interpolants A I(x0) ∧ T(x0, x1) ∧ B T(x1, x2) . . . T(xk−1, xk) ∧ ¬P(xk) If BMC query is unsat, obtain the interpolant R of A and B R is a formula over the variables x1 R over-approximates the set of states reachable in one transition No bad state is reachable from R in k − 1 steps ·KAVY ·IA072 – spring 2021, May 21, 2021 9 / 15 PDR (Inductive) trace is a sequence F = [F0, . . . , Fn] of states where F0 = I Fi (x) ∧ T(x, x ) =⇒ Fi+1(x ) for all 0 ≤ i < n A trace is monotone if Fi =⇒ Fi+1 for all 0 ≤ i < n Two phases: block bad states, push forward good states ·KAVY ·IA072 – spring 2021, May 21, 2021 10 / 15 Important pieces BMC searches for counter-examples (reachable ¬P-states) k-induction uses multiple transitions to get more information about system Interpolation can over-approximate states reachable in one (or more) transitions PDR takes a set of good states and find its inductive subset (in the form of a monotonic inductive trace) ·KAVY ·IA072 – spring 2021, May 21, 2021 11 / 15 (K)AVY - intuition ·KAVY ·IA072 – spring 2021, May 21, 2021 12 / 15 KAVY Algorithm (main loop) F, N ← [I], 0 # Do BMC constrained to F while True: let U ≡ F0(x0) ∧ T(x0, x1) ∧ . . . ∧ FN(xn) ∧ T(xn, xn+1) ∧ ¬P(xn+1) if sat(U): return unsafe (+ cex) (i, k) ← frame_to_extend(F) [F0, . . . , FN+1] ← extend(F, (i, k)) [F0, . . . , FN+1] ← pdr_push(F) # some frame got inductive if ∃i ≤ N : Fi =⇒ ( j