協力妥当性チェッカー
CVC5
開発者スタンフォード大学とアイオワ大学
初回リリース2022 （2022年）
安定版リリース
1.2.1 [ 1 ] / 2025年1月28日 （2025年1月28日）
書かれたC++
オペレーティング·システムWindows、Linux、macOS
タイプ定理証明器
ライセンスBSD 3節
Webサイトcvc5 .github .io

コンピュータサイエンスと数理論理学において、協調妥当性チェッカー(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 ]、（co）データ型[ 12 ]、シーケンス（動的配列のモデル化に使用）[ 13 ] 、有限集合と関係[ 14 ]、[ 15 ]、分離論理[ 16 ]、非解釈関数などの理論をサポートしています。cvc5はさらに有限体をサポートしています。[ 17 ]

標準的なSMTとSyGuSによる解決に加えて、cvc5は、式Aと結合して目標式Cを証明できる式Bを構築する問題である、帰納的推論をサポートしています。[ 18 ] [ 19 ]

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

アプリケーション

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

参考文献

  1. ^ 「リリース cvc5-1.2.1 · cvc5/cvc5」 . GitHub . 2025年2月12日閲覧。
  2. ^バレット、クラーク; ティネッリ、チェーザレ (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{{citation}}: CS1 maint: ISBNによる作業パラメータ（リンク）
  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). 「産業用SMTソルバーにおける柔軟な証明生成」 . Blanchette, Jasmin; Kovács, Laura; Pattinson, Dirk (編). 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. ^
  8. ^ Liang, Tianyi; Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark; Deters, Morgan (2014). 「文字列と正規表現の理論のためのDPLL(T)理論ソルバー」 . Biere, Armin; Bloem, Roderick (編).コンピュータ支援検証. コンピュータサイエンス講義ノート. 第8559巻. シュプリンガー・インターナショナル・パブリッシング. 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). 「2つのソルバーの物語：ビットベクトルへの積極的アプローチと遅延アプローチ」 . Biere, Armin; Bloem, Roderick (編).コンピュータ支援検証. コンピュータサイエンス講義ノート. 第8559巻. シュプリンガー・インターナショナル・パブリッシング. pp.  680– 695. doi : 10.1007/978-3-319-08867-9_45 . ISBN 978-3-319-08867-9。
  10. ^ブレイン、マーティン、ニーメッツ、アイナ、プレイナー、マティアス、レイノルズ、アンドリュー、バレット、クラーク、ティネッリ、チェーザレ (2019). 「浮動小数点数式の可逆性条件」。ディリグ、イシル、タシラン、セルダー（編）.コンピュータ支援検証. コンピュータサイエンス講義ノート. シュプリンガー・インターナショナル・パブリッシング. 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 (編).結合システムの最前線. コンピュータサイエンス講義ノート. 第9322巻. シュプリンガー・インターナショナル・パブリッシング. 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ソルバーにおける（共）データ型の決定手順」 . 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。
  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). 「ベクトルについての推論：シーケンス理論を法とした充足可能性」 . 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 (編).自動推論. コンピュータサイエンス講義ノート. 第9706巻. シュプリンガー・インターナショナル・パブリッシング. 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 . コンピュータサイエンス講義ノート. 第10395巻. 出版社: 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). 「SMTにおける分離ロジックのための決定手順」 . 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 .
  17. ^ 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 .
  18. ^ Reynolds, Andrew; Barbosa, Haniel; Larraz, Daniel; Tinelli, Cesare (2020-05-30). 「列挙構文誘導合成によるスケーラブルなアブダクションアルゴリズム」.自動推論. コンピュータサイエンス講義ノート. 第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. ^
  21. ^ Berman, Shmuel (2021-10-17). 「例によるプログラミング：ループプログラムの合成」 . 2021 ACM SIGPLAN 国際会議「システム、プログラミング、言語、アプリケーション：人類のためのソフトウェア」コンパニオンプロシーディングス. SPLASH コンパニオン 2021. ニューヨーク州ニューヨーク：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 (編).コンピュータ支援検証. コンピュータサイエンス講義ノート. 第13371巻. 出版社: Springer International Publishing. pp.  3– 18. doi : 10.1007/978-3-031-13185-1_1 . ISBN 978-3-031-13185-1. S2CID  251447649 .
  24. ^
  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 Bounded Model Checker」 . Á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 (編).システムの構築と分析のためのツールとアルゴリズム. コンピュータサイエンス講義ノート. 第13243巻. 出版社: Springer International Publishing. pp.  415–442。土井: 10.1007/978-3-030-99524-9_24。ISBN 978-3-030-99524-9. S2CID  247857361 .
  • バレット, クラーク; コンウェイ, クリストファー L.; デターズ, モーガン; ハダレアン, リアナ; ジョバノヴィッチ, デヤン; キング, ティム; レイノルズ, アンドリュー; ティネリ, チェーザレ (2011). "CVC4" . ゴパラクリシュナン, ガネーシュ; カディール, シャズ (編).コンピュータ支援検証. コンピュータサイエンス講義ノート. 第6806巻. ベルリン, ハイデルベルク: シュプリンガー. pp.  171– 177. doi : 10.1007/978-3-642-22110-1_14 . ISBN 978-3-642-22110-1。
「 https://en.wikipedia.org/w/index.php?title=Cooperating_Validity_Checker&oldid=1328728733」より取得