論文の概要: Augmenting Interpolation-Based Model Checking with Auxiliary Invariants (Extended Version)
- arxiv url: http://arxiv.org/abs/2403.07821v2
- Date: Fri, 25 Oct 2024 14:10:42 GMT
- ステータス: 翻訳完了
- システム内更新日: 2024-10-28 13:35:01.125960
- Title: Augmenting Interpolation-Based Model Checking with Auxiliary Invariants (Extended Version)
- Title（参考訳）: 補助不変量を用いた補間モデル検査の拡張(拡張版)
- Authors: Dirk Beyer, Po-Chun Chien, Nian-Ze Lee,
- Abstract要約: モデル検査に外部不変量を注入する拡張型検証アルゴリズムを提案する。
インジェクション不変により安全性の証明に必要なクエリ数が削減され,実行時の効率が向上することがわかった。
- 参考スコア（独自算出の注目度）: 4.309079367183251
- License:
- Abstract: Software model checking is a challenging problem, and generating relevant invariants is a key factor in proving the safety properties of a program. Program invariants can be obtained by various approaches, including lightweight procedures based on data-flow analysis and intensive techniques using Craig interpolation. Although data-flow analysis runs efficiently, it often produces invariants that are too weak to prove the properties. By contrast, interpolation-based approaches build strong invariants from interpolants, but they might not scale well due to expensive interpolation procedures. Invariants can also be injected into model-checking algorithms to assist the analysis. Invariant injection has been studied for many well-known approaches, including k-induction, predicate abstraction, and symbolic execution. We propose an augmented interpolation-based verification algorithm that injects external invariants into interpolation-based model checking (McMillan, 2003), a hardware model-checking algorithm recently adopted for software verification. The auxiliary invariants help prune unreachable states in Craig interpolants and confine the analysis to the reachable parts of a program. We implemented the proposed technique in the verification framework CPAchecker and evaluated it against mature SMT-based methods in CPAchecker as well as other state-of-the-art software verifiers. We found that injecting invariants reduces the number of interpolation queries needed to prove safety properties and improves the run-time efficiency. Consequently, the proposed invariant-injection approach verified difficult tasks that none of its plain version (i.e., without invariants), the invariant generator, or any compared tools could solve.
- Abstract（参考訳）: ソフトウェアモデルチェックは難しい問題であり、関連する不変値を生成することは、プログラムの安全性を証明するための重要な要素である。
プログラム不変量は、データフロー解析に基づく軽量な手順やクレイグ補間を用いた集中的な手法など、様々な方法で得ることができる。
データフロー解析は効率的に実行されるが、しばしばその性質を証明するには弱すぎる不変量を生成する。
対照的に、補間に基づくアプローチは、補間物から強い不変性を構築するが、高価な補間手順のため、うまくスケールしない可能性がある。
不変性は、分析を支援するためにモデルチェックアルゴリズムに注入することもできる。
不変インジェクションは、k-インダクション、述語抽象、記号実行など、よく知られた多くのアプローチで研究されている。
ソフトウェア検証に最近採用されたハードウェアモデル検査アルゴリズムである補間モデル検査(McMillan, 2003)に外部不変量を注入する補間モデル検証アルゴリズムを提案する。
補助不変量(英語版)はクレイグ補間子における到達不能状態のプルーーンを支援し、解析をプログラムの到達可能な部分に限定する。
提案手法を検証フレームワーク CPAchecker に実装し,CPAchecker の成熟した SMT ベースの手法や,その他の最先端のソフトウェア検証手法と比較した。
インジェクション不変性は安全性の証明に必要な補間クエリ数を減らし,実行時の効率を向上することがわかった。
その結果、提案された不変インジェクションアプローチは、通常のバージョン(つまり不変でない)、不変生成子、あるいは比較ツールが解決できない難しいタスクを検証した。
関連論文リスト
- Sample-efficient Bayesian Optimisation Using Known Invariances [56.34916328814857]
バニラと制約付きBOアルゴリズムは、不変目的を最適化する際の非効率性を示す。
我々はこれらの不変カーネルの最大情報ゲインを導出する。
核融合炉用電流駆動システムの設計に本手法を用い, 高性能溶液の探索を行った。
論文 参考訳（メタデータ） (2024-10-22T12:51:46Z) - Learning Non-Linear Invariants for Unsupervised Out-of-Distribution Detection [5.019613806273252]
非線型不変量学習が可能な正規化フロー様アーキテクチャからなるフレームワークを提案する。
提案手法は, 広範囲なU-OODベンチマークにおいて, 最先端の結果を得る。
論文 参考訳（メタデータ） (2024-07-04T16:01:21Z) - Masked Thought: Simply Masking Partial Reasoning Steps Can Improve Mathematical Reasoning Learning of Language Models [102.72940700598055]
推論タスクでは、小さなエラーでも不正確な結果にカスケードすることができる。
入力の摂動に頼らず、外部リソースの導入を避ける手法を開発した。
私たちのトレーニングアプローチでは、思考の連鎖の中で特定のトークンをランダムにマスクします。
論文 参考訳（メタデータ） (2024-03-04T16:21:54Z) - Deep Neural Networks with Efficient Guaranteed Invariances [77.99182201815763]
我々は、性能改善の問題、特にディープニューラルネットワークのサンプル複雑性に対処する。
群同変畳み込みは同変表現を得るための一般的なアプローチである。
本稿では,各ストリームが異なる変換に不変なマルチストリームアーキテクチャを提案する。
論文 参考訳（メタデータ） (2023-03-02T20:44:45Z) - Online Arbitrary Shaped Clustering through Correlated Gaussian Functions [0.0]
教師なしの方法で入力から任意の形状のクラスタを生成できる新しいオンラインクラスタリングアルゴリズムが提案されている。
このアルゴリズムは、バックプロパゲーションによるモデル最適化よりも生物学的に妥当であると見なすことができるが、実用性にはさらなる研究が必要である。
論文 参考訳（メタデータ） (2023-02-13T13:12:55Z) - An Accelerated Doubly Stochastic Gradient Method with Faster Explicit
Model Identification [97.28167655721766]
本稿では、分散正規化損失最小化問題に対する2倍加速勾配降下法(ADSGD)を提案する。
まず、ADSGDが線形収束率を達成でき、全体的な計算複雑性を低減できることを示す。
論文 参考訳（メタデータ） (2022-08-11T22:27:22Z) - Interpolation and SAT-Based Model Checking Revisited: Adoption to
Software Verification [3.9403985159394144]
有限状態遷移系の安全性を検証するために形式検証アルゴリズムが考案された。
20年経っても、このアルゴリズムはまだハードウェアモデル検査の最先端にある。
私たちの貢献は、この重要な20年前の知識ギャップを、ソフトウェア検証にアルゴリズムを採用することで埋めることです。
論文 参考訳（メタデータ） (2022-08-09T21:33:19Z) - Data-driven Numerical Invariant Synthesis with Automatic Generation of
Attributes [0.0]
数値不変合成と検証のためのデータ駆動アルゴリズムを提案する。
このアルゴリズムは、正および負の状態のサンプルから決定木を学習するためのICE-DTスキーマに基づいている。
論文 参考訳（メタデータ） (2022-05-30T09:18:37Z) - Incremental Verification of Fixed-Point Implementations of Neural
Networks [0.19573380763700707]
インクリメンタル境界モデル検査(BMC)、満足度変調理論(SMT)、不変推論を用いた新しいシンボル検証フレームワークの開発と評価を行った。
提案手法は,異なる入力画像を考慮した21の試験事例の85.8%,カバー手法に関連する特性の100%を検証・生成することができた。
論文 参考訳（メタデータ） (2020-12-21T10:03:44Z) - Global Optimization of Objective Functions Represented by ReLU Networks [77.55969359556032]
ニューラルネットワークは複雑で非敵対的な関数を学ぶことができ、安全クリティカルな文脈でそれらの正しい振る舞いを保証することは困難である。
ネットワーク内の障害を見つけるための多くのアプローチ(例えば、敵の例)があるが、これらは障害の欠如を保証できない。
本稿では,最適化プロセスを検証手順に統合し,本手法よりも優れた性能を実現する手法を提案する。
論文 参考訳（メタデータ） (2020-10-07T08:19:48Z) - Joint Contrastive Learning with Infinite Possibilities [114.45811348666898]
本稿では,新しい確率論的モデリングによるコントラスト学習における最近の発展の有用性について考察する。
コントラスト学習(Joint Contrastive Learning, JCL)という,コントラスト学習の特定の形態を導出する。
論文 参考訳（メタデータ） (2020-09-30T16:24:21Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。