論文の概要: An Efficient VCGen-based Modular Verification of Relational Properties
- arxiv url: http://arxiv.org/abs/2401.08385v1
- Date: Tue, 16 Jan 2024 14:19:04 GMT
- ステータス: 処理完了
- システム内更新日: 2024-01-17 13:46:43.587184
- Title: An Efficient VCGen-based Modular Verification of Relational Properties
- Title（参考訳）: 効率的なVCGenに基づく関係特性のモジュール的検証
- Authors: Lionel Blatter, Nikolai Kosmatov, Virgile Prevosto, Pascale Le Gall
- Abstract要約: 帰納的検証は通常、単一の関数呼び出しに対して各関数の振舞いを指定する関数コントラクトに依存します。
近年の研究では,検証条件生成に依存する関係性検証手法が提案されている。
- 参考スコア（独自算出の注目度）: 1.567576360103422
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Deductive verification typically relies on function contracts that specify
the behavior of each function for a single function call. Relational properties
link several function calls together within a single specification. They can
express more advanced properties of a given function, such as non-interference,
continuity, or monotonicity, or relate calls to different functions, possibly
run in parallel, for instance, to show the equivalence of two implementations.
However, relational properties cannot be expressed and verified directly in the
traditional setting of modular deductive verification. Recent work proposed a
new technique for relational property verification that relies on a
verification condition generator to produce logical formulas that must be
verified to ensure a given relational property. This paper presents an overview
of this approach and proposes important enhancements. We integrate an optimized
verification condition generator and extend the underlying theory to show how
relational properties can be proved in a modular way, where one relational
property can be used to prove another one, like in modular verification of
function contracts. Our results have been fully formalized and proved sound in
the Coq proof assistant.
- Abstract（参考訳）: 帰納的検証は通常、単一の関数呼び出しに対する各関数の振る舞いを特定する関数コントラクトに依存する。
リレーショナルプロパティは、複数の関数呼び出しを単一の仕様内で結びつける。
彼らは与えられた関数のより高度な性質、例えば非干渉、連続性、および単調性を表現することができ、また異なる関数への呼び出しを関連付けることができ、例えば2つの実装の同値性を示すために並列に実行される。
しかし、関係性は従来のモジュラー帰納的検証の設定では直接表現や検証はできない。
近年の研究では、与えられた関係性を保証するために検証されなければならない論理式を生成するための検証条件生成装置に依存する関係性検証の新しい手法が提案されている。
本稿では,本手法の概要と重要な拡張を提案する。
我々は、最適化された検証条件生成器を統合し、その基礎となる理論を拡張し、モジュラーな方法で関係性がどのように証明できるかを示す。
我々の結果は完全形式化され、coqの証明アシスタントで証明された。
関連論文リスト
- A Refreshed Similarity-based Upsampler for Direct High-Ratio Feature Upsampling [54.05517338122698]
一般的な類似性に基づく機能アップサンプリングパイプラインが提案されている。
本稿では,セマンティック・アウェアとディテール・アウェアの両方の観点から,明示的に制御可能なクエリキー機能アライメントを提案する。
我々は,モーザイクアーティファクトを緩和する上ではシンプルだが有効であるHR特徴に対して,きめ細かな近傍選択戦略を開発する。
論文 参考訳（メタデータ） (2024-07-02T14:12:21Z) - Nonparametric Partial Disentanglement via Mechanism Sparsity: Sparse
Actions, Interventions and Sparse Temporal Dependencies [58.179981892921056]
この研究は、メカニズムのスパーシティ正則化(英語版)と呼ばれる、アンタングルメントの新たな原理を導入する。
本稿では,潜在要因を同時に学習することで,絡み合いを誘発する表現学習手法を提案する。
学習した因果グラフをスパースに規則化することにより、潜伏因子を復元できることを示す。
論文 参考訳（メタデータ） (2024-01-10T02:38:21Z) - Refining and relating fundamentals of functional theory [0.0]
ここでは、なぜ6つの同値な普遍汎函数が存在するのかを説明し、それらの間の簡潔な関係を証明し、$v$-representability の重要な概念は変数のスコープと選択に相対的であると結論付ける。
時間反転対称性を持つ系に対して、なぜ6つの同値な普遍汎函数が存在するのかを説明し、それらの間の簡潔な関係を証明し、$v$-表現可能性の重要な概念は変数のスコープと選択に相対的であると結論付ける。
論文 参考訳（メタデータ） (2023-01-24T18:09:47Z) - Relational Action Bases: Formalization, Effective Safety Verification,
and Invariants (Extended Version) [67.99023219822564]
我々はリレーショナルアクションベース(RAB)の一般的な枠組みを紹介する。
RABは両方の制限を解除することで既存のモデルを一般化する。
データ対応ビジネスプロセスのベンチマークにおいて、このアプローチの有効性を実証する。
論文 参考訳（メタデータ） (2022-08-12T17:03:50Z) - On Neural Architecture Inductive Biases for Relational Tasks [76.18938462270503]
合成ネットワーク一般化(CoRelNet)と呼ばれる類似度分布スコアに基づく簡単なアーキテクチャを導入する。
単純なアーキテクチャの選択は、分布外一般化において既存のモデルより優れていることが分かる。
論文 参考訳（メタデータ） (2022-06-09T16:24:01Z) - Adaptive n-ary Activation Functions for Probabilistic Boolean Logic [2.294014185517203]
マッチングやアリティ向上の活性化関数を用いて,任意の論理を単一層で学習できることが示される。
我々は,非ゼロパラメータの数を信念関数の有効アリティに直接関連付ける基礎を用いて,信念表を表現する。
これにより、パラメータの間隔を誘導することで論理的複雑性を低減する最適化アプローチが開かれる。
論文 参考訳（メタデータ） (2022-03-16T22:47:53Z) - Using Partial Monotonicity in Submodular Maximization [13.23676270963484]
多くの標準部分モジュラーアルゴリズムに対して、単調性比に依存する新しい近似保証を証明できることが示される。
これにより、映画レコメンデーション、二次プログラミング、画像要約の一般的な機械学習応用に対する近似比が向上する。
論文 参考訳（メタデータ） (2022-02-07T10:35:40Z) - First Power Linear Unit with Sign [0.0]
バイオニクスの直感的な意味を持ちながら、一般的な逆操作によって啓蒙される。
PFPLUSと呼ばれるより一般化された型に表される関数を2つのパラメータで拡張する。
論文 参考訳（メタデータ） (2021-11-29T06:47:58Z) - A New Representation of Successor Features for Transfer across
Dissimilar Environments [60.813074750879615]
多くの実世界のRL問題は、異なるダイナミクスを持つ環境間での移動を必要とする。
ガウス過程を用いて後継特徴関数をモデル化する手法を提案する。
我々の理論的解析は、この手法の収束と、後続特徴関数のモデル化における有界誤差を証明している。
論文 参考訳（メタデータ） (2021-07-18T12:37:05Z) - Concave Aspects of Submodular Functions [0.0]
部分モジュラー関数はエントロピーや相互情報などの情報理論の量を一般化する。
部分モジュラ函数も凹凸の兆候を示す。
上界に付随する超微分と多面体を特徴付け, 微分を用いた部分モジュラーの最適条件を提供する。
論文 参考訳（メタデータ） (2020-06-27T17:06:24Z) - From Sets to Multisets: Provable Variational Inference for Probabilistic
Integer Submodular Models [82.95892656532696]
サブモジュール関数は機械学習やデータマイニングにおいて広く研究されている。
本研究では,整数部分モジュラ函数に対する連続DR-部分モジュラ拡張を提案する。
整数部分モジュラー関数によって定義される新しい確率モデルを定式化する。
論文 参考訳（メタデータ） (2020-06-01T22:20:45Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。