論文の概要: Augmenting Interpolation-Based Model Checking with Auxiliary Invariants
(Extended Version)
- arxiv url: http://arxiv.org/abs/2403.07821v1
- Date: Tue, 12 Mar 2024 17:02:53 GMT
- ステータス: 処理完了
- システム内更新日: 2024-03-13 20:31:55.206487
- Title: Augmenting Interpolation-Based Model Checking with Auxiliary Invariants
(Extended Version)
- Title(参考訳): 補助不変量を用いた補間モデル検査の拡張(拡張版)
- Authors: Dirk Beyer, Po-Chun Chien, and Nian-Ze Lee
- Abstract要約: モデル検査に外部不変量を注入する拡張型検証アルゴリズムを提案する。
インジェクション不変により安全性の証明に必要なクエリ数が削減され,実行時の効率が向上することがわかった。
- 参考スコア(独自算出の注目度): 4.309079367183251
- License: http://creativecommons.org/licenses/by/4.0/
- 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(参考訳): ソフトウェアモデルチェックは難しい問題であり、関連する不変量を生成することは、プログラムの安全性を証明する上で重要な要素である。
プログラム不変量は、データフロー解析に基づく軽量な手順やcraig補間を用いた集中的な手法など、様々なアプローチによって得られる。
データフロー解析は効率的に実行されるが、しばしば特性を証明するには弱すぎる不変量を生成する。
対照的に、補間ベースのアプローチは補間体から強い不変量を構築するが、高価な補間手順のためにスケールしない可能性がある。
不変量はモデルチェックアルゴリズムに注入して解析を支援することもできる。
不変インジェクションは、k-インダクション、述語抽象、シンボリック実行など、多くのよく知られたアプローチで研究されている。
ソフトウェア検証に最近採用されたハードウェアモデル検査アルゴリズムである補間モデル検査(McMillan, 2003)に外部不変量を注入する補間モデル検証アルゴリズムを提案する。
補助不変量はクレイグ補間における到達不能な状態の探索を助け、解析をプログラムの到達可能な部分に限定する。
提案手法を検証フレームワーク CPAchecker に実装し,CPAchecker の成熟した SMT ベースの手法や,その他の最先端のソフトウェア検証手法と比較した。
インジェクション不変性は安全性の証明に必要な補間クエリ数を減らし,実行時の効率を向上することがわかった。
その結果、提案された不変インジェクションアプローチは、通常のバージョン(つまり不変でない)、不変生成子、あるいは比較ツールが解決できない難しいタスクを検証した。
関連論文リスト
- Automatic Program Instrumentation for Automatic Verification (Extended
Technical Report) [0.0]
帰納的検証とソフトウェアモデルチェックでは、特定の仕様言語構造を扱うことが問題となる。
本稿では,様々なアドホックなアプローチを仮定する統一検証パラダイムとして,インスツルメンテーションを提案する。
我々は,プログラムのアグリゲーションによる検証に適したMonoCeraツールにアプローチを実装した。
論文 参考訳(メタデータ) (2023-05-26T14:55:35Z) - 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) - Object Representations as Fixed Points: Training Iterative Refinement
Algorithms with Implicit Differentiation [88.14365009076907]
反復的洗練は表現学習に有用なパラダイムである。
トレーニングの安定性とトラクタビリティを向上させる暗黙の差別化アプローチを開発する。
論文 参考訳(メタデータ) (2022-07-02T10:00:35Z) - Data-driven Numerical Invariant Synthesis with Automatic Generation of
Attributes [0.0]
数値不変合成と検証のためのデータ駆動アルゴリズムを提案する。
このアルゴリズムは、正および負の状態のサンプルから決定木を学習するためのICE-DTスキーマに基づいている。
論文 参考訳(メタデータ) (2022-05-30T09:18:37Z) - Improving the Sample-Complexity of Deep Classification Networks with
Invariant Integration [77.99182201815763]
変換によるクラス内分散に関する事前知識を活用することは、ディープニューラルネットワークのサンプル複雑性を改善するための強力な方法である。
そこで本研究では,アプリケーションの複雑な問題に対処するために,プルーニング法に基づく新しい単項選択アルゴリズムを提案する。
本稿では,Rotated-MNIST,SVHN,CIFAR-10データセットにおけるサンプルの複雑さの改善について述べる。
論文 参考訳(メタデータ) (2022-02-08T16:16:11Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。