Software Model Checking with IC3

Beamed by Daan Leijen's Madoko

Nikolaj Bjørner
SAT/SMT Summer School 2014, Semmering

IC3 recap

  • $\vec{x}$ are state variables.

  • $m$ is a monome (a conjunction of literals).

  • $\varphi$ is a clause (a disjunction of literals).

  • Convention: $m[\vec{x}]$ is a monome over variables $\vec{x}$, $m[\vec{x}_0]$ is a renaming of the same monome $m$ to variables $\vec{x}_0$.

IC3 recap

  • $\langle \vec{x}, \Init(\vec{x}), \rho(\vec{x_0},\vec{x}), \Safe(\vec{x})\rangle$ - a transition system.
  • $\Safe$ - good states.
  • $\cF(R)[\vec{x}_0,\vec{x}]$ - forward predicate transformer.
    • Given reachable states $R$, produce “states can be reached by including another step”.
    • From Transition System: $\Init[\vec{x}_0] \ \vee \ (R(\vec{x}_0) \wedge \rho[\vec{x}_0,\vec{x}])$
    • From Horn Clauses: $\bigvee_i Body_i[\vec{x}_0,\vec{x}]$, where
      \[  R(\vec{x}) \leftarrow Body_1[\vec{x}_0,\vec{x}] \vee \ldots\vee Body_k[\vec{x}_0,\vec{x}]\]

IC3 recap

  • $R_0, R_1, \ldots, R_N$ properties of states reachable within $i$ steps.
  • $R_i$ are sets of clauses.
  • Initially $R_0 = \Init$.
  • $\Queue$ a queue of counter-example trace properties. Initially $\Queue = \emptyset$.
  • $N$ a level indication. Initially $N = 0$.

Expanding Traces

repeat until ∞

  • Candidate If for some $m$, $m \rightarrow R_N \land \neg \Safe$, then add $\langle m, N\rangle$ to $\Queue$.

  • Unfold If $R_N \rightarrow \Safe$, then set $N \leftarrow N + 1, R_{N} \leftarrow \true$.

Termination

repeat until ∞

  • Unreachable For $i < N$, if $R_i \subseteq R_{i+1}$, return Unreachable.

  • Reachable If $\langle m, 0 \rangle \in \Queue$, return Reachable.

Backtracking

repeat until ∞

  • Conflict Let $0 \leq i < N$: given a candidate model $\langle m, i+1\rangle\in\Queue$ and clause $\varphi$, such that

    • $\neg\varphi\subseteq m$,
    • $\cF(R_i \land \varphi) \rightarrow \varphi$,
      then conjoin $\varphi$ to $R_{j}$, for $j \leq i + 1$.

  • Leaf If $\langle m, i\rangle \in \Queue$, $0 < i < N$ and $m \land \cF(R_{i-1})$ is unsatisfiable, then add $\langle m, i + 1\rangle$ to $\Queue$.

Inductive Generalization

repeat until ∞

  • Induction For $0 \leq i < N$, a clause $(\varphi \lor\psi)\ \in R_i$, $\varphi\not\in R_{i+1}$, if $\cF(R_i \wedge \varphi)\rightarrow \varphi$, then conjoin $\varphi$ to $R_{j}$, for each $j \leq i + 1$.

IC3 beyond SAT

Decide - Generalized form

Decide Add $\langle m_0[\vec{x}], i\rangle$ to $\Queue$ if $\langle m[\vec{x}], i+1\rangle \in \Queue$, $m' \land m_0[\vec{x}_0] \ \rightarrow \ \cF(R_{i})[\vec{x}_0,\vec{x}] \land m$.

  • [11, 16] Model from propositional SAT check for $m \land \cF(R_{i})[\vec{x}_0,\vec{x}]$ gives (near prime implicant) $m_0$.
  • [19] Model from SMT check for arithmetical $m \land \cF(R_{i})[\vec{x}_0,\vec{x}]$ produces numerical assignment $m_0$.
  • [13, 21] Partial quantifier elimination.
  • [24] $(\exists\vec{x} \ . \ m \land \cF(R_{i})[\vec{x}_0,\vec{x}]) \ \equiv\ \bigvee_i \psi_i[\vec{x}_0]$ where $\psi_i$ are quantifier-free. Use model for $m \land \cF(R_{i})[\vec{x}_0,\vec{x}]$ to compute $\psi_i$ without expanding full disjunction.
  • [15, 20] Keep vocabulary of literals fixed (= predicate abstraction).

Loos-Weispfenning QE

  • $\varphi$ in NNF
  • $E$ set of $x = t$ atoms in $\varphi$
  • $L$ set of $x > s$ atoms in $\varphi$
  • $U$ set of $x < t$ atoms in $\varphi$
  • there are no other occurrences of $x$ in $\varphi[x]$

\[
\exists x \ . \ \varphi[x]  \equiv 
\varphi[\infty] \vee  \bigvee_{(x = t) \in E} \varphi[t] \vee \bigvee_{(x < t) \in U} \varphi[t - \epsilon]
\]

  • Note: $(x < t')[t - \epsilon] \equiv t \leq t'$
  • Pick disjunction corresponding to satisfied equality or inequality.

Decide - Generalized form

Pssst: I am replacing $m, m_0, m'$ by greek letters.

  • Decide Add $\langle \phidown[\vec{x}], i\rangle$ to $\Queue$, if
    • $\langle \varphi[\vec{x}], i+1\rangle \in \Queue$,
    • $\phidown[\vec{x}_0] \wedge \theta[\vec{x}]$ is consistent,
    • $\theta[\vec{x}] \rightarrow \varphi[\vec{x}]$, and
    • $\phidown[\vec{x}_0] \land \theta[\vec{x}] \ \rightarrow\ \cF(R_{i})(\vec{x}_0,\vec{x})$

Interpolating Conflict

Conflict Let $0 \leq i < N$: given a candidate model $\langle m, i+1\rangle\in\Queue$ and clause $\varphi$, such that $\neg\varphi\subseteq m$, if $\cF(R_i \land \varphi) \rightarrow \varphi$, then conjoin $\varphi$ to $R_{j}$, for $j \leq i + 1$.

  • Note: $(\neg\varphi\subseteq m)$ $\equiv$ $(\varphi \rightarrow \neg m)$.
  • By monotonicity: $(\cF(R_i) \rightarrow \varphi) \ \rightarrow \ (\cF(R_i \land \varphi) \rightarrow \varphi)$.
  • Interpolation as special case: $\cF(R_i) \rightarrow \varphi, \varphi \rightarrow \neg m.$
  • Overkill for SAT (use unsat core), but for SMT may supply candidate predicates.
  • For conjunction of inequalities $m$, interpolation is “simple”.

Farkas+T Lemmas

  • $m$ is conjunction of inequalities $x \geq 6 \land y \geq 7 \land \ldots$
  • $\cF(R_i)$ is quantifier-fee formula
  • $\cF(R_i) \land m$ is unsat
  • Let $C$ be a conflict that contains literals from $m$: $C := C_m \land C'$
  • Let $r := r_m r'$ be Farkas coefficients
  • So $r\cdot C \equiv 1 < 0$
  • So $m \rightarrow \neg r'C'$
  • Return $\bigwedge \neg r'_iC'_i$ instead of $m$

Interpolating Conflict

Conflict Let $0 \leq i < N$: given a candidate model $\langle \varphi, i+1\rangle\in\Queue$ and a formula $\phiup$, such that $\cF(R_i) \to \phiup$, $\phiup \to \neg \varphi$, then conjoin $\phiup$ to $R_{j}$, for $j \leq i + 1$.

Branching

DAG Branching

Recall predicate transformer for McCarthy91:

$\cF(R_i)[x,z,r] := (x > 100 \land r = x - 10) \lor  
    (x \leq 100 \land R_i(x+11,z) \land R_i(z,r))$


Decide now spawns two children.

Decide If $\langle \varphi[\vec{x}], i+1\rangle \in \Queue$ and there are consistent $\phidown[\vec{x}_0] \land \psidown[\vec{x}_1] \land \theta[\vec{x}]$ such that $\theta[\vec{x}] \rightarrow \varphi[\vec{x}]$ and $\phidown[\vec{x}_0] \land \psidown[\vec{x}_1] \land \theta[\vec{x}] \ \rightarrow\ 
\cF(R_{i})[\vec{x}_0,\vec{x}_1, \vec{x}]$, then add $\langle \phidown[\vec{x}], i\rangle$, $\langle \psidown[\vec{x}], i\rangle$ to $\Queue$.

Searching a DAG

We also have to take DAG unfolding into acount.

Base Mark $\langle \varphi[\vec{x}], i\rangle \in \Queue$ if $i = 0$ or if there is a consistent $\theta[\vec{x}]$ such that $\theta[\vec{x}] \rightarrow \varphi[\vec{x}]$ and $\theta[\vec{x}] \ \rightarrow\ 
\cF(R_{i})[\vec{x}_0,\vec{x}_1, \vec{x}]$.
Close Mark $\langle \varphi[\vec{x}], i+1\rangle$ if all children are marked.
Reachable If $\langle \varphi, 0 \rangle$ is marked, return Reachable.

Searching a DAG

  • Model from propositional SAT check for $m \land \cF(R_{i})[\vec{x}_0,\vec{x}_1, \vec{x}]$ gives us $\phidown, \psidown$.
  • Idea: Model from SMT check for arithmetical $m \land \cF(R_{i})[\vec{x}_0,\vec{x}]$ produces numerical assignments.
  • Effect: models explored in branches are far from prime $\Rightarrow$ lemmas become too weak.

Search with Under-approximations [24]

  • Instead of tracking progress using marking use under approximations.
  • Maintain $U_0 := \false, U_1, U_2, \ldots, U_N$ of under approximations.
  • Recall that $R_0 := \false, R_1, R_2, \ldots, R_N$ are over approximations.
  • Satisfying
    • $R_i \leftarrow U_i \rightarrow U_{i+1} \rightarrow \cF(U_i)$.

Search with Under-approximations

Decide and Conflict pushing a goal $\langle \varphi, i+1 \rangle$ over $\cF(\_,\_)$

\[\xymatrix @-0.5em{
& \cF(R_i,R_i) \\
\cF(U_i,R_i) \ar[ur] & & \cF(R_i,U_i) \ar[ul] \\
& \cF(U_i,U_i) \ar[ul] \ar[ur]
}\]
  • If $\varphi \land \cF(R_i,R_i) \equiv \bot$, then goal cannot be reached.
  • If $\varphi \land \cF(U_i,U_i) \not\equiv \bot$, then goal can be reached.
  • Otherwise case split on $\varphi \land \cF(U_i,R_i)$.

Search with Under-approximations

Reachable If $U_N \land \neg\Safe$ is satisfiable, then return Reachable.
Decide$_1$ For $0 \leq i < N$ for $\langle \varphi, i+1\rangle \in \Queue$, add $\langle \phidown, i\rangle$ to $\Queue$ if:
- $\cF(U_i, U_i) \land \varphi \equiv \bot$.
- $\cF(R_i, U_i) \land \varphi \not\equiv \bot$.
- $\phidown[\vec{x}_0] \rightarrow \exists \vec{x}_1, \vec{x} \ . \ \cF(R_i,U_i) \land \varphi$ 
- $\phidown$ is disjoint from $\psi$ for every $\langle \psi, i\rangle \in \Queue$.
Decide$_2$ For $0 \leq i < N$ for $\langle \varphi, i+1\rangle \in \Queue$, add $\langle \phidown, i\rangle$ to $\Queue$ if:
- $\cF(R_i, U_i) \land \varphi \equiv \bot$ .
- $\cF(R_i, R_i) \land \varphi \not\equiv \bot$.
- $\phidown[\vec{x}_1] \rightarrow \exists \vec{x}_0, \vec{x} \ . \ \cF(R_i,R_i) \land \varphi$
- $\phidown$ is disjoint from $\psi$ for every $\langle \psi, i\rangle \in \Queue$.
Close For $0 \leq i < N$ for $\langle \varphi, i+1\rangle \in \Queue$, if $\cF(U_i,U_i) \land \varphi$ is satisfiable, but $U_{i+1} \land \varphi$ is unsatsifiable, then update $U_{i+1} := U_{i+1} \ \lor \ \psi$, where $\psi \ \rightarrow \ \exists \vec{x}_0, \vec{x}_1 \ . \ \cF(U_i,U_i) \land \varphi$.

Recursion-free Horn Clauses

  • Interpolation in standard form is a special case of Horn Clause solving.
    (1)
    \[A(\vec{a},\vec{x}) \rightarrow I(\vec{x}), \ \ \ 
I(\vec{x}) \rightarrow B(\vec{x},\vec{b})\]
  • IC3 (sans Inductive Generalization) produces as side-effect solutions that are interpolants.
  • Interpolants are quaint, almost beautiful [2, 4, 12].

Research Progress and Challenges

  • [14] Quantitative queries
  • [9] Quantified invariants for arrays
  • [6] Game of Horn: Existentials and well-orderings
  • [10] Higher-order recursion schema solving as IC3 + Horn + Data-types
  • Relations to acceleration, fold-unfold, saturation/infinite descent
  • Bit-vectors, arrays [3], strings [1], non-linear arithmetic, EPR [8], Algebraic data-types, …

Bibliography

  • [7, 17] Proof Rules for Program Verification and Horn Clauses.
  • [21] IC3 for timed automata
  • [13] IC3 with partial quantifier elimination
  • [19] IC3 with interpolating conflicts and Horn Clauses
  • [22] IC3 for Petri nets
  • [26] Interpolation for Horn Clauses
  • [23] $\mu$Z + abstraction
  • [5] $\mu$Z pre-processing and benchmaks
  • [24] IC3 + under-approximations for Horn Clause solving
  • [18] $\mu$Z + abstraction for bit-vectors
  • [25] Lazy annotation revisited
  • [15] IC3 + implicit predicate abstraction
  • [20] IC3 + predicate abstraction for EPR.

Madoko daan

  • Madoko is a A Fast Scholarly Markdown Processor,
  • intuitive and powerful integration of markdown and LaTeX,
  • browser and Azure based - no installation,
  • immediate preview,
  • real-time collaborative editing,
  • is written in Koka,
  • is by Daan Leijen, Microsoft Research,
  • Madoko is funct-ing slick!

References

[1]  Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukás Holik, Ahmed Rezine, Philipp Rümmer, and Jari Stenman. String constraints for verification. In CAV, pages 150–166, 2014. 🔎
[2]  Aws Albarghouthi and Kenneth L. McMillan. Beautiful interpolants. In CAV, pages 313–329, 2013. 🔎
[3]  Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, and Natasha Sharygina. Safari: Smt-based abstraction for arrays with interpolants. In CAV, pages 679–685, 2012. 🔎
[4]  Sam Bayless, Celina Val, Thomas Ball, Holger Hoos, and Alan Hu. Efficient Modular SAT Solving for IC3. 2013. 🔎
[5]  Josh Berdine, Nikolaj Bjørner, Samin Ishtiaq, Jael E. Kriener, and Christoph M. Wintersteiger. Resourceful reachability as horn-la. In LPAR, pages 137–146, 2013. 🔎
[6]  Tewodros A. Beyene, Swarat Chaudhuri, Corneliu Popeea, and Andrey Rybalchenko. A constraint-based approach to solving games on infinite graphs. In POPL, pages 221–234, 2014. 🔎
[7]  Nikolaj Bjørner, Kenneth L. McMillan, and Andrey Rybalchenko. Program verification as satisfiability modulo theories. In SMT@IJCAR, pages 3–11, 2012. 🔎
[8]  Nikolaj Bjørner, Arie Gurfinkel, Konstantin Korovin, and Ori Lahav. Instantiations, Zippers and EPR Interpolation. In Short paper at LPAR 19, 2013a. 🔎
[9]  Nikolaj Bjørner, Kenneth L. McMillan, and Andrey Rybalchenko. On solving universally quantified horn clauses. In SAS, pages 105–125, 2013b. 🔎
[10]  Nikolaj Bjørner, Kenneth L. McMillan, and Andrey Rybalchenko. Higher-order program verification as satisfiability modulo theories with algebraic data-types. CoRR, abs/1306.5264, 2013c. 🔎
[11]  Aaron R. Bradley. SAT-Based Model Checking without Unrolling. In VMCAI, pages 70–87, 2011. 🔎
[12]  Hana Chockler, Alexander Ivrii, and Arie Matsliah. Computing interpolants without proofs. In Armin Biere, Amir Nahir, and Tanja Vos, editors, Hardware and Software: Verification and Testing, volume 7857 of Lecture Notes in Computer Science, pages 72–85. Springer Berlin Heidelberg, 2013. 🔎
[13]  Alessandro Cimatti and Alberto Griggio. Software Model Checking via IC3. In CAV, pages 277–293, 2012. 🔎
[14]  Alessandro Cimatti, Alberto Griggio, Sergio Mover, and Stefano Tonetta. Parameter synthesis with ic3. In FMCAD, pages 165–168, 2013. 🔎
[15]  Alessandro Cimatti, Alberto Griggio, Sergio Mover, and Stefano Tonetta. IC3 Modulo Theories via Implicit Predicate Abstraction. In TACAS, pages 46–61, 2014. 🔎
[16]  Niklas Eén, Alan Mishchenko, and Robert K. Brayton. Efficient implementation of property directed reachability. In FMCAD, pages 125–134, 2011. 🔎
[17]  Sergey Grebenshchikov, Nuno P. Lopes, Corneliu Popeea, and Andrey Rybalchenko. Synthesizing software verifiers from proof rules. In PLDI, 2012. 🔎
[18]  Arie Gurfinkel, Anton Belov, and Joao Marques-Silva. Synthesizing safe bit-precise invariants. In TACAS, pages 93–108, 2014. 🔎
[19]  Krystof Hoder and Nikolaj Bjørner. Generalized Property Directed Reachability. In SAT, pages 157–171, 2012. 🔎
[20]  Shachar Itzhaky, Nikolaj Bjørner, Thomas W. Reps, Mooly Sagiv, and Aditya V. Thakur. Property-directed shape analysis. In CAV, pages 35–51, 2014. 🔎
[21]  Roland Kindermann, Tommi A. Junttila, and Ilkka Niemelä. SMT-Based Induction Methods for Timed Systems. In FORMATS, pages 171–187, 2012. 🔎
[22]  Johannes Kloos, Rupak Majumdar, Filip Niksic, and Ruzica Piskac. Incremental, inductive coverability. In CAV, pages 158–173, 2013. 🔎
[23]  Anvesh Komuravelli, Arie Gurfinkel, Sagar Chaki, and Edmund M. Clarke. Automatic Abstraction in SMT-Based Unbounded Software Model Checking. In CAV, pages 846–862, 2013. 🔎
[24]  Anvesh Komuravelli, Arie Gurfinkel, and Sagar Chaki. Smt-based model checking for recursive programs. In CAV, pages 17–34, 2014. 🔎
[25]  Kenneth L. McMillan. Lazy annotation revisited. In CAV, pages 243–259, 2014. 🔎
[26]  Philipp Rümmer, Hossein Hojjat, and Viktor Kuncak. Disjunctive interpolants for horn-clause verification. In CAV, pages 347–363, 2013. 🔎