理論による充足可能性

コンピュータサイエンスと数理論理学において、理論を法とする充足可能性問題( SMT ) は、数式が充足可能かどうかを判断する問題です。これは、ブール充足可能性問題(SAT) を、実数、整数、および/またはリスト、配列、ビットベクトル、文字列などのさまざまなデータ構造を含む、より複雑な数式に一般化します。この名前は、これらの式が、等式を持つ一階述語論理(多くの場合、量指定子は許可されません) の特定の形式理論の範囲内で (「法」で) 解釈されるという事実に由来しています。SMTソルバーは、入力の実用的なサブセットに対して SMT 問題を解くことを目的としたツールです。Z3やcvc5などの SMT ソルバーは、自動定理証明、プログラム分析、プログラム検証、ソフトウェアテストなど、コンピュータサイエンスの幅広いアプリケーションのビルディングブロックとして使用されています。

ブール充足可能性は既にNP完全であるため、SMT問題は典型的にはNP困難であり、多くの理論では決定不可能である。研究者たちは、どの理論または理論のサブセットが決定可能なSMT問題につながるか、そして決定可能なケースの計算複雑性を研究している。結果として得られる決定手順は、多くの場合SMTソルバーに直接実装される。例えば、プレスブルガー算術の決定可能性を参照のこと。SMTは制約充足問題、つまり制約プログラミングへの形式化されたアプローチと考えることができる。

用語と例

正式には、 SMT インスタンスは一階述語論理における式であり、関数および述語記号の一部には追加の解釈があり、 SMT はそのような式が充足可能かどうかを判断する問題です。言い換えれば、2値変数の一部が適切な非2値変数の集合に対する述語に置き換えられたブール充足可能性問題(SAT) のインスタンスを想像してください。述語は、非2値変数の2値関数です。述語の例には、線形不等式(例: ) や、解釈されない項および関数記号を含む等式 (例: 、ここでは 2 つの引数を取る未指定の関数) などがあります。これらの述語は、割り当てられたそれぞれの理論に従って分類されます。たとえば、実変数に関する線形不等式は線形実算術の理論の規則を使用して評価されますが、解釈されない項および関数記号を含む述語は等式を持つ解釈されない関数の理論(空理論と呼ばれることもある) の規則を使用して評価されます。その他の理論としては、配列とリスト構造の理論（コンピュータプログラムのモデリングと検証に有用）やビットベクトルの理論（ハードウェア設計のモデリングと検証に有用）などがあります。また、サブ理論も考えられます。例えば、差分論理は線形算術のサブ理論であり、各不等式は変数 と および定数 に対してという形に制限されます。 3×+2y−z≥4{\displaystyle 3x+2y-z\geq 4}f（f（あなた、v）、v）＝f（あなた、v）{\displaystyle f(f(u,v),v)=f(u,v)}f{\displaystyle f}×−y>c{\displaystyle xy>c}×{\displaystyle x}y{\displaystyle y}c{\displaystyle c}

上記の例は、不等式に対する線形整数演算の使用を示しています。他にも以下のような例があります。

  • 満足度:満足度を判定します。×∨（y∧¬z）{\displaystyle x\vee (y\wedge \neg z)}
  • 配列アクセス: A [0] = 5となる配列Aの値を検索します 。
  • ビットベクトル演算: xとyが異なる 3 ビット数値であるかどうかを判断します。
  • 解釈されない関数:およびとなるようなxとyの値を見つけます。 f（×）＝2{\displaystyle f(x)=2}グラム（×）＝3{\displaystyle g(x)=3}

ほとんどの SMT ソルバーは、そのロジックの量指定子のないフラグメントのみをサポートします。

自動定理証明との関係

SMTによる解決と自動定理証明（ATP）の間には、かなりの重複があります。一般的に、自動定理証明器は量指定子を含む完全な一階述語論理のサポートに重点を置いているのに対し、SMTソルバーは様々な理論（解釈された述語記号）のサポートに重点を置いています。ATPは量指定子を多く含む問題に優れており、SMTソルバーは量指定子を含まない大規模な問題に優れています。[ 1 ]この境界線は曖昧であり、一部のATPはSMT-COMPに、一部のSMTソルバーはCASCにそれぞれ参加しています。[ 2 ]

表現力

SMTインスタンスは、ブールSATインスタンスの一般化であり、様々な変数の集合を様々な基礎理論の述語に置き換えたものです。SMT式は、ブールSAT式よりもはるかに豊富なモデリング言語を提供します。例えば、SMT式を使用すると、マイクロプロセッサのデータパス操作をビットレベルではなくワードレベルで モデル化できます。

比較すると、解答セットプログラミングも述語（より正確には、原子式から作成された原子文）に基づいています。SMTとは異なり、解答セットプログラミングには量指定子がなく、線形算術や差分論理などの制約を容易に表現できません。解答セットプログラミングは、解釈されない関数の自由理論に帰着するブール問題に最適です。解答セットプログラミングにおいて32ビット整数をビットベクトルとして実装することは、初期のSMTソルバーが直面したのと同じ問題のほとんどに悩まされます。つまり、 x  +  y  =  y  +  xのような「自明な」恒等式を推論することが困難です。

制約論理プログラミングは線形算術制約をサポートしますが、その理論的枠組みは全く異なります。SMTソルバーは高階論理の式を解くためにも拡張されています。[ 3 ]

ソルバーアプローチ

SMTインスタンスを解決する初期の試みでは、SMTインスタンスをブールSATインスタンスに変換し（例えば、32ビット整数変数を適切な重みを持つ32個のシングルビット変数にエンコードし、「プラス」などのワードレベルの演算をビット上の低レベルの論理演算に置き換える）、この式をブールSATソルバーに渡すという手法が用いられました。このアプローチはイーガーアプローチ（またはビットブラスト）と呼ばれ、SMT式を同等のブールSAT式に前処理することで、既存のブールSATソルバーを「そのまま」使用でき、時間の経過とともにパフォーマンスと容量の向上を活用できるというメリットがあります。一方、基礎理論の高水準意味論の喪失は、ブールSATソルバーが「自明な」事実（例えば整数加算）を発見するために必要以上に多くの作業を必要とすることを意味します。この観察から、 DPLLスタイルの探索によるブール推論と、特定の理論の述語の論理積（AND）を扱う理論特化型ソルバー（Tソルバー）を緊密に統合した、多くのSMTソルバーが開発されました。このアプローチは、レイジーアプローチと呼ばれています。[ 4 ]×+y＝y+×{\displaystyle x+y=y+x}

DPLL(T) [ 5 ]と呼ばれるこのアーキテクチャは、ブール推論の役割を DPLL ベースの SAT ソルバーに委ね、この SAT ソルバーは明確に定義されたインターフェースを介して理論 T のソルバーと対話します。理論ソルバーは、式のブール検索空間を探索する際に、SAT ソルバーから渡された理論述語の論理積の実現可能性をチェックするだけで済みます。ただし、この統合がうまく機能するためには、理論ソルバーが伝播と競合分析に参加できなければなりません。つまり、既に確立されている事実から新しい事実を推論でき、理論の競合が生じたときには実行不可能性の簡潔な説明を提供できなければなりません。言い換えると、理論ソルバーは増分的でバックトラック可能でなければなりません。

決定可能な理論

研究者たちは、どの理論または理論のサブセットが決定可能なSMT問題につながるか、そして決定可能なケースの計算複雑性を研究しています。完全な一階述語論理は半決定可能でしかないため、事実上命題論理のような一階述語論理の断片に対する効率的な決定手続きを見つけようとする研究があります。[ 6 ]

もう一つの研究分野には、有理数と整数の線形演算、固定幅ビットベクトル、[ 7 ]浮動小数点演算（多くの場合、ビットブラスト、つまりビットベクトルへの縮小によってSMTソルバーに実装される）、 [ 8 ] [ 9 ]文字列、[ 10 ] (co)-データ型、[ 11 ]シーケンス（動的配列をモデル化するために使用）、[ 12 ]有限集合と関係、[ 13 ] [ 14 ]分離論理、[ 15 ]有限体、[ 16 ]および解釈されない関数など、特殊な決定可能理論の開発が含まれます。

ブール単調理論は、効率的な理論伝播と矛盾分析をサポートする理論のクラスであり、DPLL(T)ソルバー内での実用的な使用を可能にする。[ 17 ]単調理論はブール変数のみをサポートし（ブール変数は唯一の種類である）、そのすべての関数と述語pは公理に従う。

p（…、b私−1、0、b私+1、…）⟹p（…、b私−1、1、b私+1、…）{\displaystyle p(\ldots,b_{i-1},0,b_{i+1},\ldots)\implies p(\ldots,b_{i-1},1,b_{i+1},\ldots)}

単調理論の例としては、グラフ到達可能性、凸包の衝突検出、最小カット、計算木論理などが挙げられる。[ 18 ]すべてのDatalogプログラムは単調理論として解釈できる。[ 19 ]

決定不可能な理論に対するSMT

一般的なSMTアプローチのほとんどは決定可能理論をサポートしています。しかし、航空機とその挙動など、現実世界の多くのシステムは、超越関数を含む実数上の非線形演算によってのみモデル化できます。この事実は、SMT問題を非線形理論に拡張し、例えば次の方程式が充足可能かどうかを判定するといった問題への応用を促します。

（罪⁡（×）3＝コス⁡（ログ⁡（y）⋅×）∨b∨−×2≥2.3y）∧（¬b∨y<−34.4∨経験⁡（×）>y×）{\displaystyle {\begin{array}{lr}&(\sin(x)^{3}=\cos(\log(y)\cdot x)\vee b\vee -x^{2}\geq 2.3y)\wedge \left(\neg b\vee y<-34.4\vee \exp(x)>{y \over x}\right)\end{array}}}

どこ

b∈B、×、y∈R。{\displaystyle b\in {\mathbb {B} },x,y\in {\mathbb {R} }.}

しかしながら、このような問題は一般には決定不可能である。（一方、実閉体の理論、ひいては実数の完全な一階理論は、量指定子除去を用いて決定可能である。これはアルフレッド・タルスキによるものである。）加算（乗算は含まない）を含む自然数の一階理論はプレスブルガー算術と呼ばれ、これも決定可能である。定数による乗算は入れ子状の加算として実装できるため、多くのコンピュータプログラムの算術はプレスブルガー算術を用いて表現でき、結果として決定可能な式が得られる。

実数上の決定不可能な算術理論の理論原子のブール結合を扱うSMTソルバーの例としては、非線形最適化パケットを（必然的に不完全な）従属理論ソルバーとして採用した古典的なDPLL(T)アーキテクチャを採用したABsolver [ 20 ]、DPLL SAT解決と区間制約伝播を統合したiSATアルゴリズムに基づくiSAT [ 21 ] 、およびcvc5 [ 22 ]がある。

ソルバー

以下の表は、利用可能な多くのSMTソルバーの機能の一部をまとめたものです。「SMT-LIB」列はSMT-LIB言語との互換性を示します。「対応」とマークされているシステムの多くは、SMT-LIBの旧バージョンのみをサポートしているか、言語の一部しかサポートしていない可能性があります。「CVC」列はCVC言語のサポートを示します。「DIMACS」列はDIMACS形式のサポートを示します。

プロジェクトは機能やパフォーマンスだけでなく、周囲のコミュニティの存続可能性、プロジェクトに対する継続的な関心、ドキュメント、修正、テスト、機能強化に貢献する能力においても異なります。

プラットフォーム 特徴 注記
名前 OS ライセンス SMT-LIB CVC ディマックス 組み込まれた理論 API SMT-COMP [1]
ABソルバー リナックスCPLバージョン1.2 いいえ はい 線形演算、非線形演算 C++いいえ DPLLベース
アルトエルゴLinux、Mac OS、WindowsCeCILL-C ( LGPLとほぼ同等) 部分的なv1.2とv2.0 いいえ いいえ 空理論、線形整数および有理数演算、非線形演算、多態配列、列挙データ型、AC シンボル、ビットベクトル、レコードデータ型、量指定子OCaml2008 ML風の多態的一階入力言語、SATソルバーベース、理論を法とした推論のためのショスタク風とネルソン・オッペン風のアプローチを組み合わせたもの
バルセロジック リナックス独自の バージョン1.2 空論、差異論理C++2009 DPLLベースの合同閉包
ビーバー Linux、WindowsBSDバージョン1.2 いいえ いいえ ビットベクトル OCaml2009 SATソルバーベース
ブールレクター リナックスマサチューセッツ工科大学バージョン1.2 いいえ いいえ ビットベクトル、配列 C2009 SATソルバーベース
CVC3 リナックスBSDバージョン1.2 はい 空理論、線形算術、配列、タプル、型、レコード、ビットベクトル、量指定子C / C++2010 HOLへの証明出力
CVC4 Linux、Mac OS、Windows、FreeBSDBSDはい はい 有理数および整数線形演算、配列、タプル、レコード、帰納的データ型、ビットベクトル、文字列、および解釈されない関数シンボル上の等価性 C++ 2021 バージョン1.8は2021年5月にリリースされました
cvc5 Linux、Mac OS、WindowsBSDはい はい 有理数および整数線形演算、配列、タプル、レコード、帰納的データ型、ビットベクトル、有限体、文字列、シーケンス、バッグ、および解釈されない関数シンボル上の等価性 C++、Python、Java 2021 バージョン1.0は2022年4月にリリースされました
意思決定手順ツールキット（DPT） リナックスアパッチいいえ OCamlいいえ DPLLベース
アイサット リナックス独自の いいえ 非線形演算 いいえ DPLLベース
数学SAT Linux、Mac OS、Windows独自の はい はい 空理論、線形演算、非線形演算、ビットベクトル、配列 C / C++、Python、Java2010 DPLLベース
ミニスムット リナックスLGPL部分的なv2.0 非線形演算 OCaml2010 SATソルバーベース、Yicesベース
ノルン 文字列制約のSMTソルバー
オープンコグリナックスAGPLいいえ いいえ いいえ 確率論理、算術、関係モデルC++、Scheme、Pythonいいえ 部分グラフ同型性
オープンSMT Linux、Mac OS、WindowsGPLv3部分的なv2.0 はい 空理論、差分、線形算術、ビットベクトル C++2011 遅延SMTソルバー
raSAT リナックス GPLv3 バージョン2.0 実数および整数の非線形演算 2014年、2015年 区間制約伝播のテストと中間値定理の拡張
サテーン ? 独自の バージョン1.2 線形演算、差分論理 なし 2009
SMTインターポール Linux、Mac OS、WindowsLGPLv3バージョン2.5 解釈されない関数、線形実数演算、線形整数演算 ジャワ2012 高品質でコンパクトな補間を生成することに重点を置いています。
SMCHR Linux、Mac OS、WindowsGPLv3いいえ いいえ いいえ 線形演算、非線形演算、ヒープ Cいいえ 制約処理ルールを使用して新しい理論を実装できます。
SMT-RAT Linux、Mac OSマサチューセッツ工科大学バージョン2.0 いいえ いいえ 線形演算、非線形演算 C++2015 SMT 準拠の実装のコレクションで構成される、戦略的かつ並列的な SMT 解決のためのツールボックス。
ソノラー Linux、Windows独自の 部分的なv2.0 ビットベクトル C2010 SATソルバーベース
槍 Linux、Mac OS、Windows独自の バージョン1.2 ビットベクトル 2008
STP Linux、OpenBSD、Windows、Mac OSマサチューセッツ工科大学部分的なv2.0 はい いいえ ビットベクトル、配列 C、C++、Python、OCaml、Java2011 SATソルバーベース
剣 リナックス独自の バージョン1.2 ビットベクトル 2009
ユークリッド リナックスBSDいいえ いいえ いいえ 空理論、線形演算、ビットベクトル、制約付きラムダ（配列、メモリ、キャッシュなど） いいえ SATソルバーベースで、Moscow MLで記述されています。入力言語はSMVモデルチェッカーです。ドキュメントも充実しています。
ベリット Linux、OS XBSD部分的なv2.0 空理論、有理数と整数の線形算術、量指定子、および解釈されない関数記号上の等式 C / C++2010 SATソルバーベースで証明を生成できる
イエスLinux、Mac OS、Windows、FreeBSDGPLv3バージョン2.0 いいえ はい 有理数および整数線形演算、ビットベクトル、配列、および解釈されない関数シンボル上の等価性 C2014 ソースコードはオンラインで入手可能
Z3定理証明器Linux、Mac OS、Windows、FreeBSDマサチューセッツ工科大学バージョン2.0 はい 空理論、線形算術、非線形算術、ビットベクトル、配列、データ型、量指定子、文字列 C / C++、. NET、OCaml、Python、Java、Haskell2011 ソースコードはオンラインで入手可能

標準化とSMT-COMPソルバー競争

SMTソルバー（および自動定理証明器。しばしば同義語として使用される用語）への標準化されたインターフェースを記述する試みは複数存在します。最も有名なのはS式に基づく言語を提供するSMT-LIB標準です。その他、多くのブールSATソルバーでサポートされているDIMACS形式や、CVC自動定理証明器で使用されるCVC形式など、広くサポートされている標準化された形式があります。

SMT-LIB形式には、標準化されたベンチマークが多数付属しており、SMTソルバー間のコンペティションであるSMT-COMPが毎年開催されています。当初、このコンペティションはコンピュータ支援検証会議（CAV）[ 23 ] [ 24 ]内で開催されていましたが、2020年現在では、国際自動推論合同会議（IJCAR）に所属するSMTワークショップの一環として開催されています。[ 25 ]

アプリケーション

SMTソルバーは、プログラムの正しさを証明する検証、シンボリック実行に基づくソフトウェアテスト、そして可能なプログラム空間を探索してプログラムフラグメントを生成する合成の両方に役立ちます。ソフトウェア検証以外にも、SMTソルバーは型推論[ 26 ] [ 27 ]や、核兵器管理におけるアクターの信念のモデリングを含む理論的シナリオのモデリングにも使用されています。[ 28 ]

検証

コンピュータプログラムのコンピュータ支援検証では、SMTソルバーがよく使用されます。一般的な手法としては、前提条件、事後条件、ループ条件、アサーションをSMT式に変換し、すべてのプロパティが成立するかどうかを判定します。

Z3 SMT ソルバーをベースに構築された検証ツールは数多く存在します。Boogieは、Z3 を使用して単純な命令型プログラムを自動チェックする中間検証言語です。並行 C 用のVCC検証ツールは Boogie を使用するほか、命令型オブジェクトベース プログラム用のDafny 、並行プログラム用のChalice、C# 用のSpec#も使用します。F *は依存型言語であり、証明を見つけるために Z3 を使用します。コンパイラはこれらの証明を実行して、証明付きバイトコードを生成します。Viper検証インフラストラクチャは、検証条件を Z3 にエンコードします。sbvライブラリは、Haskell プログラムの SMT ベースの検証を提供し、ユーザーは Z3、ABC、Boolector、cvc5、MathSAT、Yices などのソルバーから選択できます。

Alt-Ergo SMTソルバーをベースに構築された検証ツールも数多く存在します。成熟したアプリケーションの一覧を以下に示します。

多くのSMTソルバーは、 SMTLIB2と呼ばれる共通インターフェース形式を実装しています（このようなファイルは通常、拡張子「.smt2」を持ちます）。LiquidHaskellツールは 、cvc5、MathSat、Z3など、S​​MTLIB2準拠の任意のソルバーを使用できる、Haskell用のリファインメント型ベースの検証ツールを実装しています。

シンボリック実行ベースの分析とテスト

SMTソルバーの重要な用途の一つは、プログラムの解析とテスト（例えば、コンコリックテスト）のためのシンボリック実行であり、特にセキュリティ上の脆弱性の発見を目的としています。このカテゴリのツールの例としては、 Microsoft ResearchのSAGE、KLEE、S2E、Tritonなどが挙げられます。シンボリック実行アプリケーションに使用されているSMTソルバーには、Z3、STP（Wayback Machineで2015年4月6日にアーカイブ）、Z3strファミリーのソルバー、Boolectorなどがあります。

インタラクティブな定理証明

SMTソルバーはRocq [ 29 ]やIsabelle/HOL [ 30 ]などの証明支援システムと統合されている。

参照

注記

  1. ^ Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C. (2013-06-01). 「Sledgehammer を SMT ソルバーで拡張する」 . Journal of Automated Reasoning . 51 (1): 109– 128. doi : 10.1007/s10817-013-9278-5 . ISSN  1573-0670 . ATP と SMT ソルバーは互いに補完的な強みを持っています。前者は量指定子をよりエレガントに扱い、後者は大規模で主に基礎的な問題に優れています。
  2. ^ Weber, Tjark; Conchon, Sylvain; Déharbe, David; Heizmann, Matthias; Niemetz, Aina; Reger, Giles (2019-01-01). "The SMT Competition 2015–2018" . Journal on Satisfiability, Boolean Modeling and Computation . 11 (1): 221– 259. doi : 10.3233/SAT190123 . S2CID 210147712 .近年、SMTソルバーはCASCで、ATPはSMT-COMPで競合しており、SMT-COMPとCASCの境界線が曖昧になってきています。 
  3. ^ Barbosa, Haniel; Reynolds, Andrew; El Ouraoui, Daniel; Tinelli, Cesare; Barrett, Clark (2019). 「SMTソルバーの高階論理への拡張」 .自動演繹 – CADE 27: 第27回自動演繹国際会議、ブラジル・ナタール、2019年8月27～30日、議事録. Springer. pp.  35– 54. doi : 10.1007/978-3-030-29436-6_3 . ISBN 978-3-030-29436-6。S2CID  85443815。 hal-02300986。
  4. ^ Bruttomesso, Roberto; Cimatti, Alessandro; Franzén, Anders; Griggio, Alberto; Hanna, Ziyad; Nadel, Alexander; Palti, Amit; Sebastiani, Roberto (2007). 「困難な産業検証問題のための遅延型階層化SMT( $\mathcal{BV}$ )ソルバー」 . Damm, Werner; Hermanns, Holger (編). Computer Aided Verification . Lecture Notes in Computer Science. Vol. 4590. ベルリン、ハイデルベルク：Springer. pp.  547– 560. doi : 10.1007/978-3-540-73368-3_54 . ISBN 978-3-540-73368-3。
  5. ^ Nieuwenhuis, R.; Oliveras, A.; Tinelli, C. (2006)、「SATおよびSAT Modulo理論の解決：抽象Davis-Putnam-Logemann-Loveland手順からDPLL(T)へ」（PDF）、Journal of the ACM、vol. 53、pp.  937– 977、doi：10.1145/1217856.1217859、S2CID 14058631 
  6. ^ de Moura, Leonardo; Bjørner, Nikolaj (2008年8月12日～15日). 「DPLLと置換セットを用いた命題論理の効果的な決定」 . Armando, Alessandro; Baumgartner, Peter; Dowek, Gilles (編).自動推論. 第4回国際自動推論合同会議, シドニー, ニューサウスウェールズ州, オーストラリア. コンピュータサイエンスに関する講義ノート. ベルリン, ハイデルベルク: Springer. pp.  410– 425. doi : 10.1007/978-3-540-71070-7_35 . ISBN 978-3-540-71070-7。
  7. ^ Hadarean, Liana; Bansal, Kshitij; Jovanović, Dejan; Barrett, Clark; Tinelli, Cesare (2014). 「2つのソルバーの物語：ビットベクトルへの積極的アプローチと遅延アプローチ」 . Biere, Armin; Bloem, Roderick (編).コンピュータ支援検証. コンピュータサイエンス講義ノート. 第8559巻. シュプリンガー・インターナショナル・パブリッシング. pp.  680– 695. doi : 10.1007/978-3-319-08867-9_45 . ISBN 978-3-319-08867-9。
  8. ^ Brain, Martin; Schanda, Florian; Sun, Youcheng (2019). 「浮動小数点問題のためのより優れたビットブラストの構築」. Vojnar, Tomáš; Zhang, Lijun (編).システムの構築と分析のためのツールとアルゴリズム. 第25回国際会議, システムの構築と分析のためのツールとアルゴリズム 2019, チェコ共和国プラハ, 2019年4月6日～11日, 議事録, パートI. コンピュータサイエンスの講義ノート. Cham: Springer International Publishing. pp.  79– 98. doi : 10.1007/978-3-030-17462-0_5 . ISBN 978-3-030-17462-0. S2CID  92999474 .
  9. ^ブレイン、マーティン、ニーメッツ、アイナ、プレイナー、マティアス、レイノルズ、アンドリュー、バレット、クラーク、ティネッリ、チェーザレ (2019). 「浮動小数点数式の可逆性条件」。ディリッグ、イシル、タシラン、セルダー（編）.コンピュータ支援検証. 第31回国際会議、コンピュータ支援検証2019、ニューヨーク市、2019年7月15～18日. コンピュータサイエンスの講義ノート. シュプリンガー・インターナショナル・パブリッシング. pp.  116– 136. doi : 10.1007/978-3-030-25543-5_8 . ISBN 978-3-030-25543-5. S2CID  196613701 .
  10. ^ Liang, Tianyi; Tsiskaridze, Nestan; Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark (2015). 「非有界文字列における正規メンバーシップと長さ制約の決定手順」 . Lutz, Carsten; Ranise, Silvio (編).結合システムの最前線. コンピュータサイエンス講義ノート. 第9322巻. シュプリンガー・インターナショナル・パブリッシング. pp.  135– 150. doi : 10.1007/978-3-319-24246-0_9 . ISBN 978-3-319-24246-0。
  11. ^ Reynolds, Andrew; Blanchette, Jasmin Christian (2015). 「SMTソルバーにおける（共）データ型の決定手順」 . Felty, Amy P.; Middeldorp, Aart (編).自動演繹 - CADE-25 . Lecture Notes in Computer Science. Vol. 9195. Cham: Springer International Publishing. pp.  197– 213. doi : 10.1007/978-3-319-21401-6_13 . ISBN 978-3-319-21401-6。
  12. ^ Sheng, Ying; Nötzli, Andres; Reynolds, Andrew; Zohar, Yoni; Dill, David; Grieskamp, Wolfgang; Park, Junkil; Qadeer, Shaz; Barrett, Clark; Tinelli, Cesare (2023-09-15). 「ベクトルについての推論：シーケンス理論を法とした充足可能性」 . Journal of Automated Reasoning . 67 (3): 32. doi : 10.1007/s10817-023-09682-2 . ISSN 1573-0670 . S2CID 261829653 .  
  13. ^ Bansal, Kshitij; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare (2016). 「SMTにおける有限集合と濃度制約のための新しい決定手順」 . Olivetti, Nicola; Tiwari, Ashish (編).自動推論. コンピュータサイエンス講義ノート. 第9706巻. シュプリンガー・インターナショナル・パブリッシング. pp.  82– 98. doi : 10.1007/978-3-319-40229-1_7 . ISBN 978-3-319-40229-1。
  14. ^ Meng, Baoluo; Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark (2017). 「SMTにおけるリレーショナル制約解決」 . De Moura, Leonardo (編).自動演繹 – CADE 26 . コンピュータサイエンス講義ノート. 第10395巻. 出版社: Springer International Publishing. pp.  148– 165. doi : 10.1007/978-3-319-63046-5_10 . ISBN 978-3-319-63046-5。
  15. ^ Reynolds, Andrew; Iosif, Radu; Serban, Cristina; King, Tim (2016). 「SMTにおける分離ロジックのための決定手順」(PDF) . Artho, Cyrille; Legay, Axel; Peled, Doron (編). Automated Technology for Verification and Analysis . Lecture Notes in Computer Science. Vol. 9938. Cham: Springer International Publishing. pp.  244– 261. doi : 10.1007/978-3-319-46520-3_16 . ISBN 978-3-319-46520-3. S2CID  6753369 .
  16. ^ Ozdemir, Alex; Kremer, Gereon; Tinelli, Cesare; Barrett, Clark (2023). "Satisfiability Modulo Finite Fields" . Enea, Constantin; Lal, Akash (eds.). Computer Aided Verification . Lecture Notes in Computer Science. Vol. 13965. Cham: Springer Nature Switzerland. pp.  163– 186. doi : 10.1007/978-3-031-37703-7_8 . ISBN 978-3-031-37703-7. S2CID  257235627 .
  17. ^ Bayless, Sam; Bayless, Noah; Hoos, Holger; Hu, Alan (2015-03-04). 「SAT Modulo Monotonic Theories」 . AAAI人工知能会議論文集. 29 (1). arXiv : 1406.0043 . doi : 10.1609/aaai.v29i1.9755 . ISSN 2374-3468 . S2CID 9567647 .  
  18. ^クレンツェ、トビアス;ベイレス、サム。胡、アラン J. (2016)。「SMT による高速、柔軟、最小限の CTL 合成」。スワラット州チャウドゥリにて。ファーザン、アザデ（編）。コンピュータ支援による検証。コンピューターサイエンスの講義ノート。 Vol. 9779. チャム: Springer International Publishing。 pp.  136–156。土井: 10.1007/978-3-319-41528-4_8。ISBN 978-3-319-41528-4。
  19. ^ Bembenek, Aaron; Greenberg, Michael; Chong, Stephen (2023-01-11). 「SMTからASPへ：ソルバーベースのアプローチによるデータログ合成ルール選択問題の解決」 ACM on Programming Languages 誌7 ( POPL): 7:185–7:217. doi : 10.1145/3571200 . S2CID 253525805 . 
  20. ^ Bauer, A.; Pister, M.; Tautschnig, M. (2007)、「ハイブリッドシステムとモデルの分析のためのツールサポート」、2007年ヨーロッパ設計・自動化・テスト会議議事録 (DATE'07)、IEEEコンピュータ協会、p. 1、CiteSeerX 10.1.1.323.6807、doi : 10.1109/DATE.2007.364411、ISBN  978-3-9810801-2-4、S2CID  9159847
  21. ^ Fränzle, M.; Herde, C.; Ratschan, S.; Schubert, T.; Teige, T. (2007)、「複雑なブール構造を持つ大規模非線形算術制約システムの効率的な解決」(PDF) , Journal on Satisfiability, Boolean Modeling and Computation , 1 (3–4 JSAT Special Issue on SAT/CP Integration): 209– 236, doi : 10.3233/SAT190012
  22. ^ Barbosa, Haniel; Barrett, Clark; Brain, Martin; Kremer, Gereon; Lachnitt, Hanna; Mann, Makai; Mohamed, Abdalrhman; Mohamed, Mudathir; Niemetz, Aina; Nötzli, Andres; Ozdemir, Alex; Preiner, Mathias; Reynolds, Andrew; Sheng, Ying; Tinelli, Cesare (2022). 「cvc5: 多用途で産業用SMTソルバー」 Fisman, Dana; Rosu, Grigore (編).システムの構築と分析のためのツールとアルゴリズム、第28回国際会議。コンピュータサイエンスの講義ノート。第13243巻。Cham: Springer International Publishing. pp.  415–442。土井: 10.1007/978-3-030-99524-9_24。ISBN 978-3-030-99524-9. S2CID  247857361 .
  23. ^ Barrett, Clark; de Moura, Leonardo; Stump, Aaron (2005). 「SMT-COMP: Satisfiability Modulo Theories Competition」 . Etessami, Kousha; Rajamani, Sriram K. (eds.). Computer Aided Verification . Lecture Notes in Computer Science. Vol. 3576. Springer. pp.  20– 23. doi : 10.1007/11513988_4 . ISBN 978-3-540-31686-2。
  24. ^ Barrett, Clark; de Moura, Leonardo; Ranise, Silvio; Stump, Aaron; Tinelli, Cesare (2011). 「SMT-LIBイニシアチブとSMTの台頭：（HVC 2010 Award Talk）」. Barner, Sharon; Harris, Ian; Kroening, Daniel; Raz, Orna (編).ハードウェアとソフトウェア：検証とテスト. Lecture Notes in Computer Science. Vol. 6504. Springer. p. 3. Bibcode : 2011LNCS.6504....3B . doi : 10.1007/978-3-642-19583-9_2 . ISBN 978-3-642-19583-9。
  25. ^ "SMT-COMP 2020" . SMT-COMP . 2020年10月19日閲覧。
  26. ^ Hassan, Mostafa; Urban, Caterina; Eilers, Marco; Müller, Peter (2018). 「Python 3向けMaxSMTベース型推論」 .コンピュータ支援検証. コンピュータサイエンス講義ノート. 第10982巻. pp.  12– 19. doi : 10.1007/978-3-319-96142-2_2 . ISBN 978-3-319-96141-5。
  27. ^ Loncaric, Calvin, et al.「型推論エラーの説明のための実用的なフレームワーク」 ACM SIGPLAN Notices 51.10 (2016): 781-799.
  28. ^ボーモント, ポール; エヴァンス, ニール; ヒュース, マイケル; プラント, トム (2015). 「核兵器管理のための信頼度分析：ベイズ的信念ネットワークのSMT抽象化」. ペルヌル, ギュンター; YA ライアン, ピーター; ウェイプル, エドガー (編).コンピュータセキュリティ -- ESORICS 2015 . コンピュータサイエンス講義ノート. 第9326巻. シュプリンガー. pp.  521– 540. doi : 10.1007/978-3-319-24174-6_27 . ISBN 978-3-319-24174-6。
  29. ^ Ekici, Burak; Mebsout, Alain; Tinelli, Cesare; Keller, Chantal; Katz, Guy; Reynolds, Andrew; Barrett, Clark (2017). 「SMTCoq: SMTソルバーをCoqに統合するためのプラグイン」(PDF) . Majumdar, Rupak; Kunčak, Viktor (編). Computer Aided Verification, 29th International Conference . Lecture Notes in Computer Science. Vol. 10427. Cham: Springer International Publishing. pp.  126– 133. doi : 10.1007/978-3-319-63390-9_7 . ISBN 978-3-319-63390-9. S2CID  206701576 .
  30. ^ Blanchette, Jasmin Christian; Böhme, Sascha; Paulson, Lawrence C. (2013-06-01). 「SMTソルバーによるSledgehammerの拡張」 . Journal of Automated Reasoning . 51 (1): 109– 128. doi : 10.1007/s10817-013-9278-5 . ISSN 1573-0670 . 

参考文献

「 https://en.wikipedia.org/w/index.php?title=Satisfiability_modulo_theories&oldid=1335952733#Standardization_and_the_SMT-COMP_solver_competition」より取得