モデル検査における反例空間の構造解析

(1)

モデル検査における反例空間の構造解析

Structure Analysis on Counterexamples in Model Checking

戸田貴久

1∗ 1

_{電気通信大学}

1

_{The University of Electro-Communications}

Abstract: In model checking, when the model of a system does not satisfy a given property, users manually examine the counterexample produced by a model checker to locate the fault of the system. This task is hard even for experienced users because of many variables. This paper presents a computational framework for analyzing structural features of counterexamples.

1 はじめに

ハードウェアの設計やソフトウェアのコードは人手によって作られるので、誤りが含まれることは避けられない。今日では社会の至るところが情報化され、日常生活は高度な情報システムによって支えられているので、その安全性を保つことは大切である。モデル検査は、一定の条件下で、対象のシステムが期待された通りに正しく動作することを判定したり、誤りがあると分かった場合には、誤りに至るシステムの動作例（反例と呼ばれる）を求めたりする、自動推論手法である。反例はシステムのどこに不具合があるのかを突き止めるための手がかりになり、大変有用な情報である。実際、モデル検査は産業に広く応用され、実用的な手法として認められている。モデル検査は、誤りに至る反例を求めるところまでしか自動化されていないので、反例から設計の不具合を特定するタスクはユーザによってなされている。反例はとても長く、多くの変数からなるので、これを人手でやるのは大変煩雑で、気の滅入る作業である。それゆえ、この原因特定作業を支援するための何らかの高度な自動化機能が強く求められる。同じ研究の動機に基づく過去の研究はいくつかあるが、特定の領域に特化してその領域の知識を活用したアプローチであったり、１つの反例に対して有益な情報を解析するものであった。我々の知る限りでは、複数個の反例を対象にする研究でも、せいぜい２∼３個の反例を比較するものであった。反例は確かに有用な情報を含むが、提示された情報の中には不具合への関連度の高いものもあれば、低いものもあり、情報が整理されていない。どこに注目する ∗_{連絡先：電気通信大学大学院情報理工学研究科} 〒 182-8585 東京都調布市調布ケ丘１丁目５−１ E-mail: [email protected] かはユーザに委ねられている。さらに、１つの反例は特定の場合を表すだけなので、全体像を把握しづらい。そこで、複数の反例を計算することが考えられるが、単に反例の数を増やすだけでは、意味解釈性や簡潔性からはずっと遠のく。したがって本研究では、複数の反例から抽象度が高い情報を計算によって求めることを考える。このことを数学的に言い換えると以下のようになる。変数のとる値に関する順序関係や隣接関係によって、反例同士の間にも同様の関係性が誘導される。反例の集合は一種の空間をなすと考えられる。これを反例空間と呼ぶ。このとき、ユーザに返したい抽象的な情報として、隣り合う反例によって構成される区間、正例との境界に位置する反例、あるいは、隣り合う反例が他にない孤立した反例などがあげられる。以上を踏まえて、本研究では、反例のなす空間に特徴的な構造情報を解析する計算の枠組みを提案する。本研究の貢献は以下にまとめられる。 • 通常のモデル検査を越えた高度な反例解析をシス テマチックな形で提案する。特に、反例空間の構造解析という新しい観点を導入する。 • 同じ研究の動機に基づく関連研究はあるが、特定 ドメインに特化せず、複数の反例生成に基づく手法としては、おそらく本研究が初めてである。 • 具体的に実現可能な計算の枠組みを提示する。 本論文は以下のように構成される。次の 2 節でモデル検査の基本的な概念や用語を導入する。その後、3 節で解空間の構造解析の考え方を述べ、4 節でそのための計算の枠組みを提案する。5 節でその実装について述べる。最後に 6 節で本研究をまとめる。人工知能学会研究会資料 SIG-FPAI-B801-01

(2)

2 準備

本節では後で必要になるモデル検査の概念、用語、記法を説明する。詳細は [1] を参照されたい。モデル検査は、時間とともにシステムの内部状態が変化する動的システムの振る舞いを検査するための手法である。例を用いて以下で説明する。 nビットシフトレジスタを考える。このシステムの 状態は、長さ n のビット列として表される。そのよう に表された状態 s が与えられるとき、１回のシフト操 作により、別の状態 s0に変化する。このように状態は時間とともに変化するので、システムの状態に関して述べられた命題の真偽も時間とともに変化する。このような動的システムは、クリプキ構造と呼ばれ る四つ組 (S, I, T, l) によってモデル化される。集合 S は、システムのとりうる全ての状態の集合である。集合 Iは、システムの初期状態の集合である（ I⊆ S）。二項 関係 T は状態の間の遷移関係を表し、２状態 s, s0∈ S が (s, s0)∈ T を満たすことは、状態 s から s0に遷移可能であることを意味する。システムの状態について述べた基本的な命題（原子命題）の集合を A とするとき、 lは S からP(A) への関数であり、l(s) は状態 s におい て真である原始命題の集合を意味する。モデル検査では、例えば、 ˙い ˙つ ˙かはすべてのビットが 0 になるというようなシステムの振る舞いに関する性質（仕様）をシステムのモデルが実際に満たしているか判定する。仕様は時間について言及するので、仕様を記述するための論理は、通常の命題論理を含み、時間の様相を記述するための演算子（時相演算子）を持つ。典型的 な時相演算子は、次の時刻について言及する X, 将来 のある時刻について言及する F , 将来のすべての時刻に ついて言及する G がある。そのような論理として線形 時相論理 LTL がある。本稿で提案する手法はこの LTL を前提にする。 LTLの論理式（ LTL 式）の意味を説明するために、まずパスの概念を導入する。状態の無限列は、すべての隣接する２状態が遷移関係を満たすときパスと呼ばれる。パスはシステムを動作させたときの可能な振る舞いの１例を表している。LTL 式はパスに沿って成否が定まる。これは、ある動作では仕様が満たされ、別の動作では満たされない、という状況が起こりうることを意味する。これらのことを形式的に述べると以下のようになる。 今、LTL 式 f とパス π = (s0, s1, s2, . . .)が与えられる とする。パス π の i 番以降の部分を πi_{と表す。すな} わち、πi_{= (s} i, si+1, . . .)である。このとき、fが π に 沿って成立すること（ π|= f と書く）は、論理式の構 造に関して以下のように定義される。まず、f が時相 演算子 X, F , G のいづれかが適用された形のとき、 • π |= Xg ⇔ π1_{|= g} • π |= F g ⇔ ∃i ∈ N : πi_{|= g} • π |= Gg ⇔ ∀i ∈ N : πi_{|= g} である（簡単のため他の時相演算子の説明は省く）。f が演算子∨ や ∧ を用いて表されるときは、命題論理の 通常の意味にしたがって • π |= g ∨ h ⇔ π |= g または π |= h • π |= g ∧ h ⇔ π |= g かつ π |= h と定義される。f が原始命題 p∈ A であった場合は、 • π |= p ⇔ p ∈ l(s0) と定義される。最後に、f = ¬g と表される場合は、 ¬F g ≡ G¬g, ¬Gg ≡ F ¬g, ¬Xg ≡ X¬g を用いること で、結局、原始命題の否定¬p の意味 π |= ¬p ⇔ p 6∈ l(s0)に帰着される。 定義 1 LTL モデル検査問題は、LTL 式 f とクリプキ 構造 M が与えられるとき、M の初期状態から始まる すべてのパス π に対して π|= f が成立するか判定する 問題である。 LTLモデル検査問題は PSPACE 完全であり計算コストが高いので、その近似として有界モデル検査が提案されている。本稿の提案手法は有界モデル検査を土台とする。有界モデル検査では、あらかじめ検査の範囲を限定して、その範囲の上だけで性質の検査を行う。それゆえ完全な検証を行うものではない。むしろ有界モデル検査は、システムに誤りが含まれる場合にその誤りを説明する動作例を素早く発見するための実用的な手法として広く認められている。以下、有界モデル検査についてより詳しく述べる。有界モデル検査の大きな特徴は、初期状態から一定回数の遷移で到達できる状態だけに着目することである。本稿ではこの遷移回数を限度と呼ぶ。ここで、たとえ有限個の状態であっても、無限の状態列（パス）が含まれることがあることに注意されたい。これを見るために、 k回の遷移で得られた状態列 s0, . . . , skを考える。仮に skの次の遷移先が s0から skまでのいづれかの状態 sl であるとせよ。u := (s0, . . . , sl−1)と v := (sl, . . . , sk) と表すとき、パス π = uvω_{を表現できる。与えられた} パスがこのように表されるとき (k, l)ループ（あるい は、単に kループ）と呼ぶ。 それでは、有界モデル検査における LTL 式 f の意 味を説明する。fが限度 k でパス π に沿って成立する （ π |=k f と書く）ことは、以下のように定義される。 パス π が k ループならば、π|=k f ⇔ π |= f である； そうでないならば、π |=k f ⇐ π |=0k fである。ここ

(3)

で、π|=i k fは π における現在状態のインデックス i と 限度 k をパラメータとして用いる関係であり、論理式 の構造に関して以下のように定義される。f が時相演 算子 X, F, G のいづれかが適用された形のとき、 • π |=i kXg⇔ i < k かつ π |= i+1 k g • π |=i kF g⇔ ∃j, i ≤ j ≤ k. π |= j k g • π |=i kGg⇔ 常に偽 である。その他の場合は、非有界の場合と本質的には変わりなく、 • π |=i kg∨ h ⇔ π |= i k gまたは π|= i kh • π |=i kg∧ h ⇔ π |= i k gかつ π|= i k h • π |=i kp⇔ p ∈ l(si) • π |=i k¬p ⇔ p 6∈ l(si) である（ p∈ A）。 有界モデル検査問題は定義 1 と同様に定義される。 与えられた問題が誤りと判明した場合には、π|=kfが 成立しないパス π が存在し、しかも k + 1 個の状態変 数によって有限的な表現を持つ。これは、仕様 f に反 するシステムの動作例であるから、仕様への反例と呼ばれる。反例は、システムのモデルのどこに不具合があったのかを突き止めるための手立てになる。有界モデル検査問題は co-NP 完全であり、問題を否定することで得られるパスの存在に関する判定問題を 命題論理の充足可能性判定問題（ SAT ）に帰着して解 くことができる。事実、典型的な解法では、元のモデル検査問題が偽のとき、その時に限り命題論理式 CNF が真となるように CNF 符号化を与え、SAT ソルバーを呼び出して解いている。SAT ソルバーから得られる充足変数割り当ては、元の問題の反例に対応し、変数変換を経由して反例が得られる。現代の SAT ソルバーの実用上の高い効率性により、有界モデル検査の実用性は支えられていると言っても過言ではない。

3 反例空間の構造解析

本節では、本研究の中心的なコンセプトや概念を説明する。我々は有界モデル検査問題の反例のなす集合に興味がある。反例を構成する変数は整数値をとるかもしれないし、グラフの頂点かもしれない。いづれにせよ、モデル検査における変数がとる値の間には順序関係や隣接関係など何らかの数学的構造が定まっていることが多い。 A // R1 // 3 33 33 33 33 33 33 R2 // B R3 // EE D in dst src out R1 10? 01? R2 R1 1 ? ? ? ? ? R3 R2 10? ? ? ? B R3 ? ? ? 1 ? ? D R3 1 ? ? ? ? ? R2 図 1: ネットワークとルーティングテーブルモデル検査では、反例に沿って変数の値の時間変化を観察できる。もちろん、この観察は変数の構造を考慮しながら（人手で）行われる。しかし、ここで利用できる反例は 1 つだけなので、反例の変化に応じた変数の値の変化を観察することはできない。本研究が提案するのは、この反例の変化に応じた解析である。これにより、人手による原因解明を支援する自動化機能を提供したいと考えている。ネットワーク設定の検証を例にとり 1_{、本研究を説} 明する。図 1 は、3 個のルータ R1, R2, R3と 3 個の末 端節点 A, B, D からなるネットワークである。下部に パケットの転送規則がある。簡単のためパケットは dst と src の 2 つのフィールドからなり、それぞれ３ビットで表されるとする。各行がひとつの規則であり、上から順に見ていき最初に該当する規則を適用する。in はパケットを受け取ったルータを表し、out は転送先の ルータを表す。? は 0 でも 1 でも良いことを表す。した がって、R1における規則は、まず dst が 10? で src が 01?のパケットを R2に転送する；その他のパケットの うち、dst が 1 ? ? のパケットを R3に転送する；残りのパケットはどこにも転送されずに捨てられる。このようなネットワーク設定は、クリプキ構造としてモデル化できる。状態は packet と location（略して loc）からなる。packet は dst と src を表す 2 個のビット列 packet.dst と packet.src からなる。loc は、計 6 個のネットワーク節点とパケットが棄却されたことを表す特別な節点 drop のうちいづれかの値をとる。パケッ トは最初 A の位置にあり、各ルータでの転送規則に応 じてパケットの位置が変化する。 1_{この例は [3] からとったものである。例を単純にするため、アド} レスの書き換えは省いている。

(4)

図 2: LTL 式 (1) の反例この設定の下で、LTL 式

packet.dst & 110 = 100→ F (loc = B) (1) を考えてみる。& はビット毎の積を表しているので、こ れは dst フィールドが 10? ならばいつかは B に到達で きる、という性質を表す。有界モデル検査を実行して、この性質に対する反例として例えば図 2 が求まる。src フィールドが 01? にマッチしないので、R1から R2に転送されず→ R3 → D と転送されていることが分か る。これが時間変化に基づく解析である。この例は単純なのでほとんどのことが明白であるが、 IPv4アドレスの場合 32 ビットとなり、通常ルータの個数は多く、ルーティングテーブルのサイズは大きいので、１つの反例だけでは不十分なことがある。例えば、ネットワークの場合に典型的なのは、数多くのパケットが同じ転送経路をたどって反例に至るということである。個々の特定のパケットではなく、パケットの集まりに着目することで、連続する特定のアドレス範囲に関して誤った転送設定がなされていることに気づくことができるかもしれない。これが反例の変化に基づく解析の例である。それでは、本研究の土台となる基本概念の定式化を行いたい。制約充足問題（ CSP）は 3 つ組 (X,D, C) で ある。X ={x1, . . . , xn} は有限個の変数の集合、D は 各変数 x のとる値の有限集合 D(x)（ x の定義域と呼ぶ） からなり、C は変数の上の制約からなる。 有界モデル検査の仕様に対する反例を探索する問題 Bは制約充足問題（ BCSPと書く）として定式化され、 反例は BCSPの解に 1 体 1 に対応する。ここで解とは、すべての制約を満たす変数への値割り当てであり、全空間∏D の 1 点に位置づけられる。反例空間（ある いは、解空間）は、制約充足問題として定式化された BCSPのすべての解からなる。前述のネットワーク検証の例を用いてこの定式化を 説明する。限度を k とするとき、各状態 si(0≤ i ≤ k) ごとに BCSPの変数 loci, dsti, srciがあると考える。それぞれの変数のドメインはすでに明らかであろう。制約として、例えばルーティングテーブルの先頭行に対しては loci= R1∧ dsti = 10 ?∧srci= 01?→ loci+1 = R2

という制約がある。他にも LTL 式や k ループに関する 制約がある。図 3: システム構成いくつかの変数の定義域の上には、値の間の順序関係や隣接関係などのような何らかの関係や距離が定義されていると仮定する。本研究では、反例空間の上でそのような変数に着目して、順序関係のときは連続区間を求めたり、隣接関係のときは境界値や孤立値を求めたりする。このようにユーザにとって関心のある部分に焦点を当てて、空間の特徴的な構造の解析を行うことを、本研究では反例空間の構造解析と呼ぶ。

4 計算の枠組み

本節では、反例空間の構造解析のための計算の枠組みを与える。図 3 に全体の構成を示す。

4.1 対話インターフェース

まず、ユーザとシステム内部との間に対話型のインターフェースを設ける。ユーザはシステムに対して命令を発行し、システムはその結果をユーザに返す。ユーザはこれまでの結果をもとに仮説を立て、それを確かめるための適切な命令をシステムに出す。その結果に応じて、仮説が誤りであったことを知ったり、仮説に対する確信を深めたりする。これにより、現在起きている状況をより良く理解し、不具合の特定に近づくことができる。

4.2 符号化

ユーザは高水準の言語を用いて問題をクリプキ構造や LTL 式で記述する。システム内部では、符号化部を通して、そのようなモデルや仕様を命題論理式に変換したり、逆に、命題論理変数の値割り当てからユーザレベルの変数の値割り当てに変換したりする。ここでユーザレベルの変数とは、前節で導入した制約充足問 題 BCSPの変数を意味する。

(5)

4.3 反例生成

ユーザの要求に応じて解析の対象となる反例空間を計算によって求める。すべての反例を生成するのもひとつの手ではあるが、計算コストがとても高いので現実的ではない。そこで、有界モデル検査のように、限度を定め、その範囲内ですべての反例を生成することを考える。これを有界反例生成（ Bounded Counterexample Generation; BCG）と呼ぶ。 定義 2 有界反例生成とは、限度 k, クリプキ構造 M = (S, I, T, l), LTL式 f が与えられるとき、π|=i¬f が成 立する最小の i≤ k に対して、π |=i¬f を満たす全て の反例 π を生成する問題である。 アルゴリズム 1 限度 k, LTL 式 f , クリプキ構造が与え られるときの有界反例生成 for i = 0 to k do π|=i ¬f を命題論理式 φ に変換する。 if φが充足可能 then φの全ての充足割当を出力して停止する。 end if end for アルゴリズム 1 に有界反例生成問題を解くアルゴリズムを示す。まず、反例の存在する最小レベルを発見 するために、i = 0 から順にレベルを上げながら命題論 理式 φ の充足可能性判定を繰り返す。この判定を高速 に行うために、CDCL アルゴリズムを利用する。これは現代のほとんどの SAT ソルバーがその基本アルゴリズムとして採用しているものであり、実用上の効率に定評がある。 もし φ が充足可能ならば、そのレベルに反例が少な くとも 1 個は存在することを意味する。したがって、そ の場合には、φ の全ての充足割当を列挙する。厳密に 言うと、有界反例生成問題では、ユーザレベルの変数への割当からなる反例の形で出力する必要がある。しかし、そのようなデータは、問題インスタンスごとにさまざまな型の変数値からなり、後で行う解析において扱いづらいので、ここでは論理変数に基づく形式で保持することにする。 命題論理式のすべての充足割当を列挙する問題は All-SAT と呼ばれ、[4] に主要なアルゴリズムがまとめられ、性能比較がなされている。大きく分けて、すべての充足割当を配列として出力する種類のものと、BDD と呼ばれるデータ構造として出力する種類のものとがある。これらの結果は、次に説明する反例データベースに蓄えられる。

4.4 反例データベース

反例データベースは、有界反例生成により計算された反例空間を表現する。異なる空間には異なるデータベースが作られる。前小節で述べたように、解析処理において問題インスタンスに依存せず一様な扱いを実現するために、反例はユーザレベルの変数ではなく、符号化して得られる論理変数に関するものとする。本稿で与える基本的な構造解析処理のために反例データベースに必要な唯一の要件は、指定された変数割当が反例データベースに含まれているか否かを判定するクエリ（メンバーシップクエリ）に答えられることであり、これを満たすものであればどれでも構わない。高度な構造解析を実現するためには、反例データベースの表現形式はおのずと制限される。データベースに対して必要なクエリや操作に応じて適切な表現形式を選ぶ必要がある。知識コンパイルにおいて、この点に関する理論的な解析がなされている（例えば [2]）。

4.5 構造解析

ここでは、ユーザレベルの変数と論理変数との対応を与える符号化と、反例データベースへのメンバーシップクエリとを用いて実現できるいくつかの基本的な構造解析処理を与える。他にも様々な構造解析が可能であるが、それらの実現は今後の課題として残しておく。 前節で導入したように、BCSP= (X,D, C) は、有界モデル検査の仕様に対する反例を探索する問題の制約充足問題としての定式化である。以下ではこの問題の解 空間を Sol(BCSP)と表す。1 つの解 π∈ Sol(BCSP)は、 各変数 x に D(x) の値を対応づける値割当 π : X →∪D であるが、同時に値の組として∏D の 1 点ともみなさ れることに注意されたい。着目する変数の定義域の二項関係によって、以下のように空間∏D に二項関係が誘導される。 定義 3 変数 x∈ X の定義域 D(x) には二項関係 Rxが 定義されているとする。このとき π, π0 ∈∏D に対し て Rx(π, π0)が成立するとは、

• ∀y ∈ X \ x. π(y) = π0_(y),_かつ

• Rx(π(x), π0(x)) となるときをいう。 x以外の値がすべて一致する条件は強すぎるので、特定の変数部分集合の上だけで一致するように条件を緩 和することが考えられる。変数 x の値を変更したら、 それ以降の時刻の同種の変数の値も変化してしまうから。ただ、議論が煩雑になるのでここでは上の定義を採用する。例えば、前述のネットワークの例における

(6)

パケットのように状態遷移によって値が変化しない変数（ frozen variables）に着目する場合にこの定義は意味をなすと考えられる。 Rxが順序関係≤xの場合を考える。D(x) 上の順序 関係≤xに関して π(x) の直後の値が π0(x)となるとき、 πの直後の元は π0であり、逆に π0の直前の元は π であるという。もちろんこの関係は着目する変数に対して相対的に定義されたものである。 解の列 π1, π2, . . . , πmが区間をなすとは、すべての πi, πi+1(1≤ i < m) について πiの直後の解が πi+1の ときをいい、[π1, πm]xと表す。最小値解析は、解 π と 変数 x が与えられるとき、πLの直前の元は解でなく、 [πL, π]x ⊆ Sol(BCSP)となる πLを発見する問題である。アルゴリズム 2 に解法を与える。最大値解析も同様に定義する。 アルゴリズム 2 解 π に関する最小値解析 πL ← π

while πLの直前の元 πprevが Sol(BCSP)にある do

πL ← πprev end while πLを返す。最小値解析と最大値解析を組み合わせることで、解 πを含む最長区間 [πL, πR]xを求めることができる；特 に、πL= πRとなるとき π は孤立解と分かる。

5 実装

本節では、反例空間の構造解析の実装について述べる。本研究では、有界モデル検査を行う代表的なソフトウェアの NuSMV2 を拡張させることで、提案手法を実装した。前節で説明したシステムの構成のうち、対話インターフェースと符号化は NuSMV2 の機能をほとんどそのまま利用している。また、図 3 に示されているように、通常のモデル検査の機能もそのまま利用できる。したがって、例えば、反例をトレースとして計算・表示させ、その結果に基づいて、本研究で提案した各種の構造解析を行うといったように、従来の機能と拡張機能を自由に組み合わせることができる。反例生成では、アルゴリズム 1 にしたがって SAT ソルバーと AllSAT ソルバーを呼び出すことで実現している。ここで、SAT ソルバーと同様に AllSAT ソルバーも抽象的なインターフェースを介してシステムと接続しているので、そのインターフェースに合致する限り、好みのソルバーを結合させ、呼び出すことができる。反例データベースは、反例の集合を２次元配列として表現するものと、BDD として表現するものの 2 通りを実装している。構造解析は、反例データベースと符号化を利用して、前節で説明したいくつかの基本的な処理を実現している。

6 まとめ

本稿ではモデル検査における反例のなす空間に特徴的な構造を解析するための計算の枠組みを提案した。これまでの反例の解析は、１つの反例の時間変化を観察することが基本であったのに対して、本研究で提案する解析は、反例の変化によって、着目する変数の値に関する特徴的な構造情報を計算することに基づく。これを行うために、SAT ソルバーと AllSAT ソルバーを組み合わせて、指定した範囲の反例をすべて列挙する。このように生成された反例をデータベースとして保持し、そのようなデータベースへのメンバーシップクエリと変数の符号化を介して、いくつかの基本的な構造解析処理を実現する。本研究で提案した手法により、ネットワーク設定の検証において不具合に至るパケットの連続するアドレス範囲を計算することのように、一定の意味のある計算ができることを示した。これにより、本研究が、通常のモデル検査よりも高度な知的処理を実現する上での一つの計算基盤となりうることが考えられる。ただ現在の構造解析処理では、着目する変数が時間に対して不変（いわゆる frozen variables）であることが要請されるので、この制限のない実用的な構造解析処理を考案することが今後の課題として残されている。

参考文献

[1] Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Yunshan Zhu. Symbolic model checking without bdds. In Proceedings of the 5th International Conference on Tools and Al-gorithms for Construction and Analysis of Sys-tems, TACAS ’99, pp. 193–207, Berlin, Heidel-berg, 1999. Springer-Verlag.

[2] Adnan Darwiche and Pierre Marquis. A knowl-edge compilation map. J. Artif. Int. Res., Vol. 17, No. 1, pp. 229–264, September 2002.

[3] Nuno P. Lopes, Nikolaj Bjorner, Patrice Gode-froid, and George Varghese. Network veriﬁcation in the light of program veriﬁcation. Technical re-port, Microsoft Research, September 2013.

[4] Takahisa Toda and Takehide Soh. Implementing eﬃcient all solutions sat solvers. J. Exp. Algorith-mics, Vol. 21, pp. 1.12:1–1.12:44, November 2016.