協力する妥当性チェッカー

コンピュータサイエンスと数理論理学において、Cooperating Validity Checker (CVC) は、充足可能性法理論(SMT) ソルバーのファミリーです。CVC の最新のメジャーバージョンは CVC4 と CVC5 (スタイル付きで cvc5) です。以前のバージョンには、CVC、CVC Lite、CVC3 があります。 ^{[ 2 ]} CVC4 と cvc5 はどちらも、SMT 問題を解くためのSMT-LIBおよびTPTP入力フォーマットと、プログラム合成のための SyGuS-IFフォーマットをサポートしています。CVC4 と cvc5 はどちらも、LFSC フォーマットで独立してチェックできる証明を出力できます。cvc5 はさらに Alethe および Lean 4 フォーマットもサポートしています。^[³^]^[⁴^] cvc5には、C++、Python、Javaのバインディングがあります。

CVC4は2014年から2020年にかけてSMT-COMPに出場し^{[ 5 ]}、cvc5は2021年から2022年にかけて出場した^{[ 6 ]} 。CVC4は2015年から2019年にかけてSyGuS-COMPに出場し^{[ 7 ]} 、2013年から2015年にかけてCASCに出場した。

CVC4 はDPLL(T)アーキテクチャを使用し、^{[ 8 ]}有理数と整数に対する線形算術、固定幅ビットベクトル、^{[ 9 ]}浮動小数点演算、^{[ 10 ]}文字列、^{[ 11 ]} (co)-データ型、^{[ 12 ]}シーケンス(動的配列のモデル化に使用)、 [ ¹³^]有限集合と関係、^[¹⁴^]^[¹⁵^]分離論理、^[¹⁶^]および解釈されない関数などの理論をサポートしています。cvc5 はさらに有限体^もサポートしています。^[¹⁷^]

標準的な SMT および SyGuS ソルビングに加えて、cvc5 はアブダクション推論をサポートしています。これは、目標となる式 $Cを証明するために式$ $A$ と結合できる式 $B$ を構築する問題です。^[¹⁸^]^[¹⁹^]

cvc5は、いくつかの独立したテストキャンペーンの対象となっている。^{[ 20 ]}

アプリケーション

CVC4 は再帰プログラムの合成^{[ 21 ]}やAmazon Web Services のアクセスポリシーの検証^{[ 22 ]}^{[ 23 ]}に適用されています。CVC4 と cvc5 はRocq ^{[ 24 ]}およびIsabelle ^{[ 25} ]と統合されています。CVC4は、 C 境界モデルチェッカーである CBMC ^[²⁶^]で^サポートされているバックエンド推論エンジンの 1 つです。

参考文献

↑ "Release cvc5-1.2.1 · cvc5/cvc5" . GitHub . 2025-02-12に取得.
↑ Barrett, Clark; Tinelli, Cesare (2018), "Satisfiability Modulo Theories", in Clarke, Edmund M.; Henzinger, Thomas A.; Veith, Helmut; Bloem, Roderick (eds.), Handbook of Model Checking , Cham: Springer International Publishing, pp. 305– 343, doi : 10.1007/978-3-319-10575-8_11 , ISBN 978-3-319-10575-8
↑ Barbosa, Haniel; Reynolds, Andrew; Kremer, Gereon; Lachnitt, Hanna; Niemetz, Aina; Nötzli, Andres; Ozdemir, Alex; Preiner, Mathias; Viswanathan, Arjun; Viteri, Scott; Zohar, Yoni; Tinelli, Cesare; Barrett, Clark (2022). "Flexible Proof Production in an Industrial-Strength SMT Solver" . In Blanchette, Jasmin; Kovács, Laura; Pattinson, Dirk (eds.). Automated Reasoning . Lecture Notes in Computer Science. Vol. 13385. Cham: Springer International Publishing. pp. 15–35 . doi : 10.1007/978-3-031-10769-6_3 . ISBN 978-3-031-10769-6. S2CID 250164402 .
↑ ( Barbosa et al. 2022 、p. 417)
↑ 「参加者」 . SMT-COMP . 2023-11-29取得。
↑ "SMT-COMP" . SMT-COMP . 2023-11-29に取得.
↑
- Alur, Rajeev; Fisman, Dana; Singh, Rishabh; Solar-Lezama, Armando (2016-02-02). "SyGuS-Comp'15 の結果と分析". Electronic Proceedings in Theoretical Computer Science . 202 : 3–26 . arXiv : 1602.01170 . doi : 10.4204/EPTCS.202.3 . ISSN 2075-2180 . S2CID 2086015 .
- Alur, Rajeev; Fisman, Dana; Singh, Rishabh; Solar-Lezama, Armando (2016-11-22). "SyGuS-Comp 2016: 結果と分析". Electronic Proceedings in Theoretical Computer Science . 229 : 178–202 . arXiv : 1611.07627 . doi : 10.4204/EPTCS.229.13 . ISSN 2075-2180 . S2CID 440389 .
- Alur, Rajeev; Fisman, Dana; Singh, Rishabh; Solar-Lezama, Armando (2017-11-28). "SyGuS-Comp 2017: 結果と分析". Electronic Proceedings in Theoretical Computer Science . 260 : 97–115 . arXiv : 1711.11438 . doi : 10.4204/EPTCS.260.9 . ISSN 2075-2180 . S2CID 37464992 .
↑ Liang, Tianyi; Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark; Deters, Morgan (2014). "文字列と正規表現の理論のためのDPLL(T)理論ソルバー" . Biere, Armin; Bloem, Roderick (編)『コンピュータ支援検証』Lecture Notes in Computer Science. Vol. 8559. Cham: Springer International Publishing. pp. 646–662 . doi : 10.1007/978-3-319-08867-9_43 . ISBN 978-3-319-08867-9。
↑ Hadarean, Liana; Bansal, Kshitij; Jovanović, Dejan; Barrett, Clark; Tinelli, Cesare (2014). "A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors" . In Biere, Armin; Bloem, Roderick (eds.). Computer Aided Verification . Lecture Notes in Computer Science. Vol. 8559. Cham: Springer International Publishing. pp. 680–695 . doi : 10.1007/978-3-319-08867-9_45 . ISBN 978-3-319-08867-9。
↑ Brain, Martin; Niemetz, Aina; Preiner, Mathias; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare (2019). "浮動小数点式の可逆条件". In Dillig, Isil; Tasiran, Serdar (eds.). Computer Aided Verification . Lecture Notes in Computer Science. Cham: Springer International Publishing. pp. 116–136 . doi : 10.1007/978-3-030-25543-5_8 . ISBN 978-3-030-25543-5。
↑ Liang, Tianyi; Tsiskaridze, Nestan; Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark (2015). "無制限文字列に対する正規メンバーシップと長さ制約の決定手順" . Lutz, Carsten; Ranise, Silvio (編) 『結合システムのフロンティア』所収。Lecture Notes in Computer Science. Vol. 9322. Cham: Springer International Publishing. pp. 135–150 . doi : 10.1007/978-3-319-24246-0_9 . ISBN 978-3-319-24246-0。
↑ Reynolds, Andrew; Blanchette, Jasmin Christian (2015). "SMTソルバーにおける(Co)データ型の決定手順" . Felty, Amy P.; Middeldorp, Aart (編). Automated Deduction - 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。
↑ Sheng, Ying; Nötzli, Andres; Reynolds, Andrew; Zohar, Yoni; Dill, David; Grieskamp, Wolfgang; Park, Junkil; Qadeer, Shaz; Barrett, Clark; Tinelli, Cesare (2023-09-15). "Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences" . Journal of Automated Reasoning . 67 (3): 32. doi : 10.1007/s10817-023-09682-2 . ISSN 1573-0670 . S2CID 261829653 .
↑ Bansal, Kshitij; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare (2016). "SMTにおける有限集合と基数制約のための新しい決定手順" . Olivetti, Nicola; Tiwari, Ashish (編).自動推論. Lecture Notes in Computer Science. Vol. 9706. Cham: Springer International Publishing. pp. 82–98 . doi : 10.1007/978-3-319-40229-1_7 . ISBN 978-3-319-40229-1。
↑ Meng, Baoluo; Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark (2017). "SMTにおける関係制約解決" . De Moura, Leonardo (編).自動推論 – CADE 26 . Lecture Notes in Computer Science. Vol. 10395. Cham: Springer International Publishing. pp. 148– 165. doi : 10.1007/978-3-319-63046-5_10 . ISBN 978-3-319-63046-5。
↑ Reynolds, Andrew; Iosif, Radu; Serban, Cristina; King, Tim (2016). "A Decision Procedure for Separation Logic in SMT" . In Artho, Cyrille; Legay, Axel; Peled, Doron (eds.). 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 .
↑ Ozdemir, Alex; Kremer, Gereon; Tinelli, Cesare; Barrett, Clark (2023). "有限体による充足可能性" . Enea, Constantin; Lal, Akash (編)『コンピュータ支援検証』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 .
↑ Reynolds, Andrew; Barbosa, Haniel; Larraz, Daniel; Tinelli, Cesare (2020-05-30). "列挙構文誘導合成によるアブダクションのためのスケーラブルなアルゴリズム". Automated Reasoning . Lecture Notes in Computer Science. Vol. 12166. pp. 141–160 . doi : 10.1007/978-3-030-51074-9_9 . ISBN 978-3-030-51073-2. PMC 7324138 .
↑ ( Barbosa et al. 2022 、p. 426)
↑
- Bringolf, Mauro; Winterer, Dominik; Su, Zhendong (2023-01-05). "SMTソルバーにおける不完全性バグの発見と理解" .第37回IEEE/ACM国際自動ソフトウェア工学会議（ASE '22）議事録. ニューヨーク州ニューヨーク、米国：Association for Computing Machinery. pp. 1–10 . doi : 10.1145/3551349.3560435 . ISBN 978-1-4503-9475-8. S2CID 255441416 .
- Sun, Maolin; Yang, Yibiao; Wen, Ming; Wang, Yongcong; Zhou, Yuming; Jin, Hai (2023-07-26). "履歴バグトリガー入力によるスケルトン列挙を用いたSMTソルバーの検証" . 2023 IEEE/ACM 第45回国際ソフトウェア工学会議 (ICSE) . ICSE '23. メルボルン、ビクトリア州、オーストラリア: IEEE Press. pp. 69–81 . doi : 10.1109/ICSE48619.2023.00018 . ISBN 978-1-6654-5701-9. S2CID 259860528 .
- Niemetz, Aina; Preiner, Mathias; Barrett, Clark (2022). "Murxla: SMTソルバー向けモジュール式で拡張性の高いAPIファザー" . Shoham, Sharon; Vizel, Yakir (編)『コンピュータ支援検証』Lecture Notes in Computer Science. Vol. 13372. Cham: Springer International Publishing. pp. 92–106 . doi : 10.1007/978-3-031-13188-2_5 . ISBN 978-3-031-13188-2. S2CID 251447764 .
- Kim, Jongwook; So, Sunbeom; Oh, Hakjoo (2023-07-26). "Diver: Oracle-Guided SMT Solver Testing with Unrestricted Random Mutations" . 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE) . ICSE '23. Melbourne, Victoria, Australia: IEEE Press. pp. 2224–2236 . doi : 10.1109/ICSE48619.2023.00187 . ISBN 978-1-6654-5701-9. S2CID 259860926 .
- Sun, Maolin; Yang, Yibiao; Wang, Yang; Wen, Ming; Jia, Haoxiang; Zhou, Yuming (2023). "大規模事前学習済み言語モデルによるSMTソルバー検証". 2023 第38回IEEE/ACM国際自動ソフトウェアエンジニアリング会議（ASE） . pp. 1288–1300 . doi : 10.1109/ase56229.2023.00180 . ISBN 979-8-3503-2996-4. S2CID 265055537 .
- Bringolf, Mauro (2021).数式の弱化と強化によるSMTソルバーのファズテスト（修士論文）。ETHチューリッヒ。doi : 10.3929 /ethz-b-000507582。
↑ Berman, Shmuel (2021-10-17). "Programming-by-example by programming-by-example: Synthesis of looping programs" . Companion Proceedings of the 2021 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity . SPLASH Companion 2021. New York, NY, USA: Association for Computing Machinery. pp. 19–21 . arXiv : 2108.08724 . doi : 10.1145/3484271.3484977 . ISBN 978-1-4503-9088-0. S2CID 237213485 .
↑ Backes, John; Bolignano, Pauline; Cook, Byron; Dodge, Catherine; Gacek, Andrew; Luckow, Kasper; Rungta, Neha; Tkachuk, Oksana; Varming, Carsten (2018年10月). SMTを用いたAWSアクセスポリシーのための意味論に基づく自動推論. IEEE. pp. 1–9 . doi : 10.23919/FMCAD.2018.8602994 . ISBN 978-0-9835678-8-2. S2CID 52237693 .
↑ Rungta, Neha (2022). "1日10億件のSMTクエリ（招待論文）" . Shoham, Sharon; Vizel, Yakir (編)『コンピュータ支援検証』Lecture Notes in Computer Science. Vol. 13371. Cham: Springer International Publishing. pp. 3–18 . doi : 10.1007/978-3-031-13185-1_1 . ISBN 978-3-031-13185-1. S2CID 251447649 .
↑
- CVC4の場合：Ekici, Burak; Mebsout, Alain; Tinelli, Cesare; Keller, Chantal; Katz, Guy; Reynolds, Andrew; Barrett, Clark (2017). "SMTCoq: SMTソルバーをCoqに統合するためのプラグイン" (PDF) . In Majumdar, Rupak; Kunčak, Viktor (eds.). Computer Aided Verification . 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 .
- cvc5 の場合: ( Barbosa et al. 2022 、p. 425)
- cvc5 については、Barbosa, Haniel; Keller, Chantal; Reynolds, Andrew; Viswanathan, Arjun; Tinelli, Cesare; Barrett, Clark (2023-06-03). "An Interactive SMT Tactic in Coq using Abductive Reasoning" . EPiC Series in Computing . 94. EasyChair: 11–22 . doi : 10.29007/432m . S2CID 259070258 .
↑デシャルネ、マーティン。ヴクミロヴィッチ、ペタル。ブランシェット、ジャスミン。マカリウス、ウェンゼル（2022）。「ハンマーの下の17人の証明者」。DROPS-IDN/V2/Document/10.4230/LIPIcs.ITP.2022.8。ライプニッツ国際情報学会議 (LIPIcs)。237 . Schloss-Dagstuhl - Leibniz Zentrum für Informatik: 8:1–8:18。土井：10.4230/LIPIcs.ITP.2022.8。ISBN 978-3-95977-252-5. S2CID 251322787 .
↑ Kroening, Daniel; Tautschnig, Michael (2014). "CBMC – C 境界モデルチェッカー" . In Ábrahám, Erika; Havelund, Klaus (eds.). Tools and Algorithms for the Construction and Analysis of Systems . Lecture Notes in Computer Science. Vol. 8413. Berlin, Heidelberg: Springer. pp. 389– 391. doi : 10.1007/978-3-642-54862-8_26 . ISBN 978-3-642-54862-8。

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ソルバー" . In Fisman, Dana; Rosu, Grigore (eds.). Tools and Algorithms for the Construction and Analysis of Systems . Lecture Notes in Computer Science. Vol. 13243. Cham: Springer International Publishing. pp. 415–442。土井: 10.1007/978-3-030-99524-9_24。ISBN 978-3-030-99524-9. S2CID 247857361 .
Barrett, Clark; Conway, Christopher L.; Deters, Morgan; Hadarean, Liana; Jovanović, Dejan; King, Tim; Reynolds, Andrew; Tinelli, Cesare (2011). "CVC4" . In Gopalakrishnan, Ganesh; Qadeer, Shaz (eds.). Computer Aided Verification . Lecture Notes in Computer Science. Vol. 6806. Berlin, Heidelberg: Springer. pp. 171–177 . doi : 10.1007/978-3-642-22110-1_14 . ISBN 978-3-642-22110-1。

[1] "Release cvc5-1.2.1 · cvc5/cvc5" . GitHub . 2025-02-12に取得.

[2] Barrett, Clark; Tinelli, Cesare (2018), "Satisfiability Modulo Theories", in Clarke, Edmund M.; Henzinger, Thomas A.; Veith, Helmut; Bloem, Roderick (eds.), Handbook of Model Checking , Cham: Springer International Publishing, pp. 305– 343, doi : 10.1007/978-3-319-10575-8_11 , ISBN 978-3-319-10575-8

[3] Barbosa, Haniel; Reynolds, Andrew; Kremer, Gereon; Lachnitt, Hanna; Niemetz, Aina; Nötzli, Andres; Ozdemir, Alex; Preiner, Mathias; Viswanathan, Arjun; Viteri, Scott; Zohar, Yoni; Tinelli, Cesare; Barrett, Clark (2022). "Flexible Proof Production in an Industrial-Strength SMT Solver" . In Blanchette, Jasmin; Kovács, Laura; Pattinson, Dirk (eds.). Automated Reasoning . Lecture Notes in Computer Science. Vol. 13385. Cham: Springer International Publishing. pp. 15–35 . doi : 10.1007/978-3-031-10769-6_3 . ISBN 978-3-031-10769-6. S2CID 250164402 .

[4] ( Barbosa et al. 2022 、p. 417)

[5] 「参加者」 . SMT-COMP . 2023-11-29取得。

[6] "SMT-COMP" . SMT-COMP . 2023-11-29に取得.

[7] 
Alur, Rajeev; Fisman, Dana; Singh, Rishabh; Solar-Lezama, Armando (2016-02-02). "SyGuS-Comp'15 の結果と分析". Electronic Proceedings in Theoretical Computer Science . 202 : 3–26 . arXiv : 1602.01170 . doi : 10.4204/EPTCS.202.3 . ISSN 2075-2180 . S2CID 2086015 .
Alur, Rajeev; Fisman, Dana; Singh, Rishabh; Solar-Lezama, Armando (2016-11-22). "SyGuS-Comp 2016: 結果と分析". Electronic Proceedings in Theoretical Computer Science . 229 : 178–202 . arXiv : 1611.07627 . doi : 10.4204/EPTCS.229.13 . ISSN 2075-2180 . S2CID 440389 .
Alur, Rajeev; Fisman, Dana; Singh, Rishabh; Solar-Lezama, Armando (2017-11-28). "SyGuS-Comp 2017: 結果と分析". Electronic Proceedings in Theoretical Computer Science . 260 : 97–115 . arXiv : 1711.11438 . doi : 10.4204/EPTCS.260.9 . ISSN 2075-2180 . S2CID 37464992 .

[mw6w] Alur, Rajeev; Fisman, Dana; Singh, Rishabh; Solar-Lezama, Armando (2016-02-02). "SyGuS-Comp'15 の結果と分析". Electronic Proceedings in Theoretical Computer Science . 202 : 3–26 . arXiv : 1602.01170 . doi : 10.4204/EPTCS.202.3 . ISSN 2075-2180 . S2CID 2086015 .

[mw_A] Alur, Rajeev; Fisman, Dana; Singh, Rishabh; Solar-Lezama, Armando (2016-11-22). "SyGuS-Comp 2016: 結果と分析". Electronic Proceedings in Theoretical Computer Science . 229 : 178–202 . arXiv : 1611.07627 . doi : 10.4204/EPTCS.229.13 . ISSN 2075-2180 . S2CID 440389 .

[mwAQ4] Alur, Rajeev; Fisman, Dana; Singh, Rishabh; Solar-Lezama, Armando (2017-11-28). "SyGuS-Comp 2017: 結果と分析". Electronic Proceedings in Theoretical Computer Science . 260 : 97–115 . arXiv : 1711.11438 . doi : 10.4204/EPTCS.260.9 . ISSN 2075-2180 . S2CID 37464992 .

[8] Liang, Tianyi; Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark; Deters, Morgan (2014). "文字列と正規表現の理論のためのDPLL(T)理論ソルバー" . Biere, Armin; Bloem, Roderick (編)『コンピュータ支援検証』Lecture Notes in Computer Science. Vol. 8559. Cham: Springer International Publishing. pp. 646–662 . doi : 10.1007/978-3-319-08867-9_43 . ISBN 978-3-319-08867-9。

[9] Hadarean, Liana; Bansal, Kshitij; Jovanović, Dejan; Barrett, Clark; Tinelli, Cesare (2014). "A Tale of Two Solvers: Eager and Lazy Approaches to Bit-Vectors" . In Biere, Armin; Bloem, Roderick (eds.). Computer Aided Verification . Lecture Notes in Computer Science. Vol. 8559. Cham: Springer International Publishing. pp. 680–695 . doi : 10.1007/978-3-319-08867-9_45 . ISBN 978-3-319-08867-9。

[10] Brain, Martin; Niemetz, Aina; Preiner, Mathias; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare (2019). "浮動小数点式の可逆条件". In Dillig, Isil; Tasiran, Serdar (eds.). Computer Aided Verification . Lecture Notes in Computer Science. Cham: Springer International Publishing. pp. 116–136 . doi : 10.1007/978-3-030-25543-5_8 . ISBN 978-3-030-25543-5。

[11] Liang, Tianyi; Tsiskaridze, Nestan; Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark (2015). "無制限文字列に対する正規メンバーシップと長さ制約の決定手順" . Lutz, Carsten; Ranise, Silvio (編) 『結合システムのフロンティア』所収。Lecture Notes in Computer Science. Vol. 9322. Cham: Springer International Publishing. pp. 135–150 . doi : 10.1007/978-3-319-24246-0_9 . ISBN 978-3-319-24246-0。

[12] Reynolds, Andrew; Blanchette, Jasmin Christian (2015). "SMTソルバーにおける(Co)データ型の決定手順" . Felty, Amy P.; Middeldorp, Aart (編). Automated Deduction - 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。

[13] Sheng, Ying; Nötzli, Andres; Reynolds, Andrew; Zohar, Yoni; Dill, David; Grieskamp, Wolfgang; Park, Junkil; Qadeer, Shaz; Barrett, Clark; Tinelli, Cesare (2023-09-15). "Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences" . Journal of Automated Reasoning . 67 (3): 32. doi : 10.1007/s10817-023-09682-2 . ISSN 1573-0670 . S2CID 261829653 .

[14] Bansal, Kshitij; Reynolds, Andrew; Barrett, Clark; Tinelli, Cesare (2016). "SMTにおける有限集合と基数制約のための新しい決定手順" . Olivetti, Nicola; Tiwari, Ashish (編).自動推論. Lecture Notes in Computer Science. Vol. 9706. Cham: Springer International Publishing. pp. 82–98 . doi : 10.1007/978-3-319-40229-1_7 . ISBN 978-3-319-40229-1。

[15] Meng, Baoluo; Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark (2017). "SMTにおける関係制約解決" . De Moura, Leonardo (編).自動推論 – CADE 26 . Lecture Notes in Computer Science. Vol. 10395. Cham: Springer International Publishing. pp. 148– 165. doi : 10.1007/978-3-319-63046-5_10 . ISBN 978-3-319-63046-5。

[16] Reynolds, Andrew; Iosif, Radu; Serban, Cristina; King, Tim (2016). "A Decision Procedure for Separation Logic in SMT" . In Artho, Cyrille; Legay, Axel; Peled, Doron (eds.). 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 .

[17] Ozdemir, Alex; Kremer, Gereon; Tinelli, Cesare; Barrett, Clark (2023). "有限体による充足可能性" . Enea, Constantin; Lal, Akash (編)『コンピュータ支援検証』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 .

[18] Reynolds, Andrew; Barbosa, Haniel; Larraz, Daniel; Tinelli, Cesare (2020-05-30). "列挙構文誘導合成によるアブダクションのためのスケーラブルなアルゴリズム". Automated Reasoning . Lecture Notes in Computer Science. Vol. 12166. pp. 141–160 . doi : 10.1007/978-3-030-51074-9_9 . ISBN 978-3-030-51073-2. PMC 7324138 .

[19] ( Barbosa et al. 2022 、p. 426)

[20] 
Bringolf, Mauro; Winterer, Dominik; Su, Zhendong (2023-01-05). "SMTソルバーにおける不完全性バグの発見と理解" .第37回IEEE/ACM国際自動ソフトウェア工学会議（ASE '22）議事録. ニューヨーク州ニューヨーク、米国：Association for Computing Machinery. pp. 1–10 . doi : 10.1145/3551349.3560435 . ISBN 978-1-4503-9475-8. S2CID 255441416 .
Sun, Maolin; Yang, Yibiao; Wen, Ming; Wang, Yongcong; Zhou, Yuming; Jin, Hai (2023-07-26). "履歴バグトリガー入力によるスケルトン列挙を用いたSMTソルバーの検証" . 2023 IEEE/ACM 第45回国際ソフトウェア工学会議 (ICSE) . ICSE '23. メルボルン、ビクトリア州、オーストラリア: IEEE Press. pp. 69–81 . doi : 10.1109/ICSE48619.2023.00018 . ISBN 978-1-6654-5701-9. S2CID 259860528 .
Niemetz, Aina; Preiner, Mathias; Barrett, Clark (2022). "Murxla: SMTソルバー向けモジュール式で拡張性の高いAPIファザー" . Shoham, Sharon; Vizel, Yakir (編)『コンピュータ支援検証』Lecture Notes in Computer Science. Vol. 13372. Cham: Springer International Publishing. pp. 92–106 . doi : 10.1007/978-3-031-13188-2_5 . ISBN 978-3-031-13188-2. S2CID 251447764 .
Kim, Jongwook; So, Sunbeom; Oh, Hakjoo (2023-07-26). "Diver: Oracle-Guided SMT Solver Testing with Unrestricted Random Mutations" . 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE) . ICSE '23. Melbourne, Victoria, Australia: IEEE Press. pp. 2224–2236 . doi : 10.1109/ICSE48619.2023.00187 . ISBN 978-1-6654-5701-9. S2CID 259860926 .
Sun, Maolin; Yang, Yibiao; Wang, Yang; Wen, Ming; Jia, Haoxiang; Zhou, Yuming (2023). "大規模事前学習済み言語モデルによるSMTソルバー検証". 2023 第38回IEEE/ACM国際自動ソフトウェアエンジニアリング会議（ASE） . pp. 1288–1300 . doi : 10.1109/ase56229.2023.00180 . ISBN 979-8-3503-2996-4. S2CID 265055537 .
Bringolf, Mauro (2021).数式の弱化と強化によるSMTソルバーのファズテスト（修士論文）。ETHチューリッヒ。doi : 10.3929 /ethz-b-000507582。

[mwAeQ] Bringolf, Mauro; Winterer, Dominik; Su, Zhendong (2023-01-05). "SMTソルバーにおける不完全性バグの発見と理解" .第37回IEEE/ACM国際自動ソフトウェア工学会議（ASE '22）議事録. ニューヨーク州ニューヨーク、米国：Association for Computing Machinery. pp. 1–10 . doi : 10.1145/3551349.3560435 . ISBN 978-1-4503-9475-8. S2CID 255441416 .

[mwAfQ] Sun, Maolin; Yang, Yibiao; Wen, Ming; Wang, Yongcong; Zhou, Yuming; Jin, Hai (2023-07-26). "履歴バグトリガー入力によるスケルトン列挙を用いたSMTソルバーの検証" . 2023 IEEE/ACM 第45回国際ソフトウェア工学会議 (ICSE) . ICSE '23. メルボルン、ビクトリア州、オーストラリア: IEEE Press. pp. 69–81 . doi : 10.1109/ICSE48619.2023.00018 . ISBN 978-1-6654-5701-9. S2CID 259860528 .

[mwAgQ] Niemetz, Aina; Preiner, Mathias; Barrett, Clark (2022). "Murxla: SMTソルバー向けモジュール式で拡張性の高いAPIファザー" . Shoham, Sharon; Vizel, Yakir (編)『コンピュータ支援検証』Lecture Notes in Computer Science. Vol. 13372. Cham: Springer International Publishing. pp. 92–106 . doi : 10.1007/978-3-031-13188-2_5 . ISBN 978-3-031-13188-2. S2CID 251447764 .

[mwAhU] Kim, Jongwook; So, Sunbeom; Oh, Hakjoo (2023-07-26). "Diver: Oracle-Guided SMT Solver Testing with Unrestricted Random Mutations" . 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE) . ICSE '23. Melbourne, Victoria, Australia: IEEE Press. pp. 2224–2236 . doi : 10.1109/ICSE48619.2023.00187 . ISBN 978-1-6654-5701-9. S2CID 259860926 .

[mwAiY] Sun, Maolin; Yang, Yibiao; Wang, Yang; Wen, Ming; Jia, Haoxiang; Zhou, Yuming (2023). "大規模事前学習済み言語モデルによるSMTソルバー検証". 2023 第38回IEEE/ACM国際自動ソフトウェアエンジニアリング会議（ASE） . pp. 1288–1300 . doi : 10.1109/ase56229.2023.00180 . ISBN 979-8-3503-2996-4. S2CID 265055537 .

[mwAjU] Bringolf, Mauro (2021).数式の弱化と強化によるSMTソルバーのファズテスト（修士論文）。ETHチューリッヒ。doi : 10.3929 /ethz-b-000507582。

[21] Berman, Shmuel (2021-10-17). "Programming-by-example by programming-by-example: Synthesis of looping programs" . Companion Proceedings of the 2021 ACM SIGPLAN International Conference on Systems, Programming, Languages, and Applications: Software for Humanity . SPLASH Companion 2021. New York, NY, USA: Association for Computing Machinery. pp. 19–21 . arXiv : 2108.08724 . doi : 10.1145/3484271.3484977 . ISBN 978-1-4503-9088-0. S2CID 237213485 .

[22] Backes, John; Bolignano, Pauline; Cook, Byron; Dodge, Catherine; Gacek, Andrew; Luckow, Kasper; Rungta, Neha; Tkachuk, Oksana; Varming, Carsten (2018年10月). SMTを用いたAWSアクセスポリシーのための意味論に基づく自動推論. IEEE. pp. 1–9 . doi : 10.23919/FMCAD.2018.8602994 . ISBN 978-0-9835678-8-2. S2CID 52237693 .

[23] Rungta, Neha (2022). "1日10億件のSMTクエリ（招待論文）" . Shoham, Sharon; Vizel, Yakir (編)『コンピュータ支援検証』Lecture Notes in Computer Science. Vol. 13371. Cham: Springer International Publishing. pp. 3–18 . doi : 10.1007/978-3-031-13185-1_1 . ISBN 978-3-031-13185-1. S2CID 251447649 .

[24] 
CVC4の場合：Ekici, Burak; Mebsout, Alain; Tinelli, Cesare; Keller, Chantal; Katz, Guy; Reynolds, Andrew; Barrett, Clark (2017). "SMTCoq: SMTソルバーをCoqに統合するためのプラグイン" (PDF) . In Majumdar, Rupak; Kunčak, Viktor (eds.). Computer Aided Verification . 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 .
cvc5 の場合: ( Barbosa et al. 2022 、p. 425)
cvc5 については、Barbosa, Haniel; Keller, Chantal; Reynolds, Andrew; Viswanathan, Arjun; Tinelli, Cesare; Barrett, Clark (2023-06-03). "An Interactive SMT Tactic in Coq using Abductive Reasoning" . EPiC Series in Computing . 94. EasyChair: 11–22 . doi : 10.29007/432m . S2CID 259070258 .

[mwAno] CVC4の場合：Ekici, Burak; Mebsout, Alain; Tinelli, Cesare; Keller, Chantal; Katz, Guy; Reynolds, Andrew; Barrett, Clark (2017). "SMTCoq: SMTソルバーをCoqに統合するためのプラグイン" (PDF) . In Majumdar, Rupak; Kunčak, Viktor (eds.). Computer Aided Verification . 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 .

[mwAow] vc5 の場合: ( Barbosa et al. 2022 、p. 425)

[mwApI] vc5 については、Barbosa, Haniel; Keller, Chantal; Reynolds, Andrew; Viswanathan, Arjun; Tinelli, Cesare; Barrett, Clark (2023-06-03). "An Interactive SMT Tactic in Coq using Abductive Reasoning" . EPiC Series in Computing . 94. EasyChair: 11–22 . doi : 10.29007/432m . S2CID 259070258 .

[25] デシャルネ、マーティン。ヴクミロヴィッチ、ペタル。ブランシェット、ジャスミン。マカリウス、ウェンゼル（2022）。「ハンマーの下の17人の証明者」。DROPS-IDN/V2/Document/10.4230/LIPIcs.ITP.2022.8。ライプニッツ国際情報学会議 (LIPIcs)。237 . Schloss-Dagstuhl - Leibniz Zentrum für Informatik: 8:1–8:18。土井：10.4230/LIPIcs.ITP.2022.8。ISBN 978-3-95977-252-5. S2CID 251322787 .

[26] Kroening, Daniel; Tautschnig, Michael (2014). "CBMC – C 境界モデルチェッカー" . In Ábrahám, Erika; Havelund, Klaus (eds.). Tools and Algorithms for the Construction and Analysis of Systems . Lecture Notes in Computer Science. Vol. 8413. Berlin, Heidelberg: Springer. pp. 389– 391. doi : 10.1007/978-3-642-54862-8_26 . ISBN 978-3-642-54862-8。

[ 2 ]

[

[

[ 5 ]

[ 6 ]

[ 7 ]

[ 8 ]

[ 9 ]

[ 10 ]

[ 11 ]

[ 12 ]

13

14

15

16

[

[

[

[ 20 ]

[ 21 ]

[ 22 ]

[ 23 ]

[ 24 ]

[ 25

[

アプリケーション

参考文献

関連するトピック

コンピュータサイエンス

数理論理学

充足可能性法理論

CVC4 と cvc5 はどちらも、SMT 問題を解くためのSMT-LIB