Loading article…
| 開発者 | スタンフォード大学とアイオワ大学 |
|---|---|
| 初回リリース | 2022 |
| 安定版リリース | 1.0.8 [1]
/ 2023年8月31日 |
| 書かれた | C++ |
| オペレーティング·システム | Windows、Linux、macOS |
| タイプ | 定理証明器 |
| ライセンス | BSD 3節 |
| Webサイト | 翻訳元 |
コンピュータサイエンスと数理論理学において、協調妥当性チェッカー(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 形式をサポートしています。[3] [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] 、(共)データ型[12] 、シーケンス(動的配列をモデル化するために使用) [13] 、有限集合と関係[14 ] 、[15]、 分離論理[16]、および非解釈関数などの理論をサポートしています。cvc5はさらに有限体もサポートしています。[17]
標準的なSMTとSyGuSによる解決に加えて、cvc5は、目標の式Cを証明するために式Aと結合できる式Bを構築する問題である、帰納的推論をサポートしています。[18] [19]
cvc5はいくつかの独立したテストキャンペーンの対象となっている。[20]
アプリケーション
CVC4は再帰プログラムの合成に適用されている。[21]およびAmazon Web Servicesのアクセスポリシーの検証にも適用されている。 [22] [23] CVC4とcvc5はCoq [24]およびIsabelle [ 25]と統合されている。CVC4はCBMC（C境界モデルチェッカー）がサポートするバックエンド推論エンジンの1つである。[26]
参考文献
- ^ 「リリース cvc5-1.0.8 · cvc5/cvc5」。GitHub 。 2023年11月29日閲覧。
- ^ バレット、クラーク; ティネッリ、チェーザレ (2018)、クラーク、エドモンド M.; ヘンジンガー、トーマス A.; ファイト、ヘルムート; ブルーム、ロデリック (編)、「理論による充足可能性」、モデル検査ハンドブック、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). 「産業用 SMT ソルバーにおける柔軟な証明生成」。Blanchette, Jasmin; Kovács, Laura; Pattinson, Dirk (編)。自動推論。コンピュータサイエンスの講義ノート。第 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 の結果と分析」。電子論文集、 理論計算機科学。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: 結果と分析」.理論計算機科学の電子会議. 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: 結果と分析」.理論計算機科学の電子会議. 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 (編)。コンピュータ支援検証。コンピュータサイエンスの講義ノート。第 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). 「2 つのソルバーの物語: ビット ベクトルへの積極的アプローチと遅延アプローチ」。 Biere, Armin; Bloem, Roderick (編)。コンピュータ支援検証。 コンピュータ サイエンスの講義ノート。 Vol. 8559。 Cham: Springer International Publishing。 pp. 680–695。doi :10.1007/978-3-319-08867-9_45。ISBN 978-3-319-08867-9。
- ^ ブレイン、マーティン; ニーメッツ、アイナ; プレイナー、マティアス; レイノルズ、アンドリュー; バレット、クラーク; ティネッリ、チェーザレ (2019)。「浮動小数点式の可逆性条件」。ディリグ、イシル; タシラン、セルダー (編)。コンピュータ支援検証。コンピュータサイエンスの講義ノート。チャム: シュプリンガーインターナショナルパブリッシング。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 (編)。結合システムの最前線。コンピュータサイエンスの講義ノート。第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 (編)。自動演繹 - CADE-25。コンピュータサイエンスの講義ノート。第 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). 「ベクトルについての推論：シーケンス理論による充足可能性」. 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 (編)。自動推論。コンピュータサイエンスの講義ノート。第 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 におけるリレーショナル制約の解決」。In de Moura, Leonardo (編)。自動演繹 – CADE 26。コンピュータサイエンスの講義ノート。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). 「SMT における分離ロジックの決定手順」(PDF)。 Artho, Cyrille; Legay, Axel; Peled, Doron (編)。検証と分析のための自動化技術。 コンピュータサイエンスの講義ノート。 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). 「Satisfiability Modulo Finite Fields」。Enea, Constantin; Lal, Akash (eds.) 著。コンピュータ支援検証。コンピュータサイエンスの講義ノート。第 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。
- ^ レイノルズ、アンドリュー; バルボサ、ハニエル; ララズ、ダニエル; ティネッリ、チェーザレ (2020-05-30)。「列挙構文ガイド付き合成によるアブダクションのためのスケーラブルなアルゴリズム」。自動推論。コンピュータサイエンスの講義ノート。第 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 プレス。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 (編)。コンピュータ支援検証。コンピュータサイエンスの講義ノート。第 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 ガイド付き SMT ソルバーテストと無制限ランダムミューテーション」。2023 IEEE/ACM 第 45 回国際ソフトウェア工学会議 (ICSE)。ICSE '23。メルボルン、ビクトリア州、オーストラリア: IEEE プレス。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 . 2023年11月29日閲覧。
- Bringolf, Mauro (2021). 式の弱化と強化による SMT ソルバーのファズテスト (修士論文). ETH チューリッヒ. doi :10.3929/ethz-b-000507582.
- ^ Berman, Shmuel (2021-10-17). 「プログラミング例によるプログラミング例によるループプログラムの合成」。2021 ACM SIGPLAN 国際システム、プログラミング、言語、アプリケーション会議: 人類のためのソフトウェアのコンパニオン議事録。SPLASHコンパニオン2021。ニューヨーク、ニューヨーク、米国: 計算機協会。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（編著）。コンピュータ支援検証。コンピュータサイエンスの講義ノート。第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)。Majumdar, Rupak、Kunčak, Viktor (編)。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)。「Coq での Abductive Reasoning を使用した対話型 SMT 戦術」。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。ダグシュトゥール城 - ライプニッツ情報センター。土井：10.4230/LIPIcs.ITP.2022.8。S2CID 251322787。
- ^ Kroening, Daniel; Tautschnig, Michael (2014). 「CBMC – C 境界モデルチェッカー」。Ábrahám, Erika; Havelund, Klaus (編)。システムの構築と分析のためのツールとアルゴリズム。コンピュータサイエンスの講義ノート。第 8413 巻。ベルリン、ハイデルベルク: 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 ソルバー」。Fisman, Dana; Rosu, Grigore (編)。システムの構築と分析のためのツールとアルゴリズム。Lecture Notes in Computer Science。第 13243 巻。Cham: Springer International Publishing。pp. 415–442。doi :10.1007/978-3-030-99524-9_24。番号 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」。Gopalakrishnan, Ganesh、Qadeer, Shaz (編)。Computer Aided Verification。Lecture Notes in Computer Science。Vol. 6806。ベルリン、ハイデルベルク: Springer。pp. 171–177。doi : 10.1007 / 978-3-642-22110-1_14。ISBN 978-3-642-22110-1。