論文の概要: Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification

• arxiv url: http://arxiv.org/abs/2208.05046v2
• Date: Tue, 12 Mar 2024 21:38:30 GMT
• ステータス: 処理完了
• システム内更新日: 2024-03-14 19:26:28.421213
• Title: Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification
• Title（参考訳）: 補間とSATベースのモデルチェックの再検討 ソフトウェア検証
• Authors: Dirk Beyer, Nian-Ze Lee, and Philipp Wendler
• Abstract要約: 有限状態遷移系の安全性を検証するために形式検証アルゴリズムが考案された。 20年経っても、このアルゴリズムはまだハードウェアモデル検査の最先端にある。 私たちの貢献は、この重要な20年前の知識ギャップを、ソフトウェア検証にアルゴリズムを採用することで埋めることです。
• 参考スコア（独自算出の注目度）: 3.9403985159394144
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The article "Interpolation and SAT-Based Model Checking" (McMillan, 2003) describes a formal-verification algorithm, which was originally devised to verify safety properties of finite-state transition systems. It derives interpolants from unsatisfiable BMC queries and collects them to construct an overapproximation of the set of reachable states. Although 20 years old, the algorithm is still state-of-the-art in hardware model checking. Unlike other formal-verification algorithms, such as k-induction or PDR, which have been extended to handle infinite-state systems and investigated for program analysis, McMillan's interpolation-based model-checking algorithm from 2003 has not been used to verify programs so far. Our contribution is to close this significant, two decades old gap in knowledge by adopting the algorithm to software verification. We implemented it in the verification framework CPAchecker and evaluated the implementation against other state-of-the-art software-verification techniques on the largest publicly available benchmark suite of C safety-verification tasks. The evaluation demonstrates that McMillan's interpolation-based model-checking algorithm from 2003 is competitive among other algorithms in terms of both the number of solved verification tasks and the run-time efficiency. Our results are important for the area of software verification, because researchers and developers now have one more approach to choose from.
• Abstract（参考訳）: 2003年の論文 "Interpolation and SAT-Based Model Checking" (McMillan, 2003) では、有限状態遷移システムの安全性を検証するために考案された形式検証アルゴリズムが記述されている。 補間子は不満足なBMCクエリから導出され、それらを収集して到達可能な状態の集合の過剰近似を構築する。 20年経っても、このアルゴリズムはまだハードウェアモデル検査の最先端にある。 無限状態システムを扱うために拡張され、プログラム解析のために研究されているk-inductionやPDRのような他の形式検証アルゴリズムとは異なり、2003年のマクミランの補間に基づくモデル検査アルゴリズムはプログラムの検証には使われていない。 私たちの貢献は、この重要な20年前の知識ギャップを、ソフトウェア検証にアルゴリズムを採用することで埋めることです。 検証フレームワークCPAcheckerで実装し、C言語安全検証タスクの最大のベンチマークスイート上で、最先端のソフトウェア検証技術に対する実装を評価した。 この評価は、2003年のマクミランの補間に基づくモデルチェックアルゴリズムが、解決された検証タスクの数と実行時の効率の両方の観点から、他のアルゴリズムと競合していることを示している。 私たちの結果は、ソフトウェア検証の領域において重要です。

関連論文リスト

• Formally Verified Approximate Policy Iteration [11.602089225841633]
  形式化されたアルゴリズムが実行可能で検証可能な実装にどのように洗練されるかを示す。 実装は、その実行可能性を示すために、ベンチマーク問題で評価される。 この改良の一環として,線形プログラミングソリューションを認証する検証ソフトウェアを開発した。
  論文  参考訳（メタデータ） (2024-06-11T15:07:08Z)
• Bisimulation Learning [55.859538562698496]
  我々は、大きな、潜在的に無限の状態空間を持つ状態遷移系の有限バイシミュレートを計算する。 提案手法は,実際に行われている他の最先端ツールよりも高速な検証結果が得られる。
  論文  参考訳（メタデータ） (2024-05-24T17:11:27Z)
• Augmenting Interpolation-Based Model Checking with Auxiliary Invariants (Extended Version) [4.309079367183251]
  モデル検査に外部不変量を注入する拡張型検証アルゴリズムを提案する。 インジェクション不変により安全性の証明に必要なクエリ数が削減され,実行時の効率が向上することがわかった。
  論文  参考訳（メタデータ） (2024-03-12T17:02:53Z)
• An algorithm for clustering with confidence-based must-link and cannot-link constraints [0.0]
  我々はPCCCアルゴリズム(Pairwise-Confidence-Constraints-Clustering)を導入する。 PCCCアルゴリズムは、オブジェクトのペアに提供された情報を考慮しながら、反復的にオブジェクトをクラスタに割り当てる。 既存のアルゴリズムとは異なり、我々のアルゴリズムは最大6万のオブジェクト、100のクラスタ、数百万のnot-link制約を持つ大規模インスタンスにスケールする。
  論文  参考訳（メタデータ） (2022-12-29T19:21:33Z)
• Benchmarking Quality-Dependent and Cost-Sensitive Score-Level Multimodal Biometric Fusion Algorithms [58.156733807470395]
  本稿では,BioSecure DS2 (Access Control) 評価キャンペーンの枠組み内で実施したベンチマーク研究について報告する。 キャンペーンは、約500人の中規模施設における物理的アクセス制御の適用を目標とした。 我々の知る限りでは、これは品質ベースのマルチモーダル融合アルゴリズムをベンチマークする最初の試みである。
  論文  参考訳（メタデータ） (2021-11-17T13:39:48Z)
• Machine Learning for Online Algorithm Selection under Censored Feedback [71.6879432974126]
  オンラインアルゴリズム選択(OAS)では、アルゴリズム問題クラスのインスタンスがエージェントに次々に提示され、エージェントは、固定された候補アルゴリズムセットから、おそらく最高のアルゴリズムを迅速に選択する必要がある。 SAT(Satisfiability)のような決定問題に対して、品質は一般的にアルゴリズムのランタイムを指す。 本研究では,OASのマルチアームバンディットアルゴリズムを再検討し,この問題に対処する能力について議論する。 ランタイム指向の損失に適応し、時間的地平線に依存しない空間的・時間的複雑さを維持しながら、部分的に検閲されたデータを可能にする。
  論文  参考訳（メタデータ） (2021-09-13T18:10:52Z)
• CoCoMoT: Conformance Checking of Multi-Perspective Processes via SMT (Extended Version) [62.96267257163426]
  我々はCoCoMoT(Computing Conformance Modulo Theories)フレームワークを紹介する。 まず、純粋な制御フロー設定で研究したSATベースのエンコーディングを、データ認識ケースに持ち上げる方法を示す。 次に,プロパティ保存型クラスタリングの概念に基づく新しい前処理手法を提案する。
  論文  参考訳（メタデータ） (2021-03-18T20:22:50Z)
• Incremental Verification of Fixed-Point Implementations of Neural Networks [0.19573380763700707]
  インクリメンタル境界モデル検査(BMC)、満足度変調理論(SMT)、不変推論を用いた新しいシンボル検証フレームワークの開発と評価を行った。 提案手法は,異なる入力画像を考慮した21の試験事例の85.8%,カバー手法に関連する特性の100%を検証・生成することができた。
  論文  参考訳（メタデータ） (2020-12-21T10:03:44Z)
• Adaptive Sampling for Best Policy Identification in Markov Decision Processes [79.4957965474334]
  本稿では,学習者が生成モデルにアクセスできる場合の,割引マルコフ決定(MDP)における最良の政治的識別の問題について検討する。 最先端アルゴリズムの利点を論じ、解説する。
  論文  参考訳（メタデータ） (2020-09-28T15:22:24Z)
• A Constraint-Based Algorithm for the Structural Learning of Continuous-Time Bayesian Networks [70.88503833248159]
  連続時間ベイズネットワークの構造を学習するための制約に基づく最初のアルゴリズムを提案する。 我々は,条件付き独立性を確立するために提案した,異なる統計的テストと基礎となる仮説について論じる。
  論文  参考訳（メタデータ） (2020-07-07T07:34:09Z)
• Verification and Validation of Convex Optimization Algorithms for Model Predictive Control [1.5322124183968633]
  本稿では,凸最適化アルゴリズムであるEllipsoid法とそのコード実装の形式的検証について述べる。 これらのコードプロパティと証明の適用性と制限も提示される。 数値安定性の制御に使用できるアルゴリズムの修正について述べる。
  論文  参考訳（メタデータ） (2020-05-26T09:18:14Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。