論文の概要: Bottoms Up for CHCs: Novel Transformation of Linear Constrained Horn Clauses to Software Verification

• arxiv url: http://arxiv.org/abs/2404.15215v1
• Date: Tue, 23 Apr 2024 16:46:27 GMT
• ステータス: 処理完了
• システム内更新日: 2024-04-24 13:12:44.810484
• Title: Bottoms Up for CHCs: Novel Transformation of Linear Constrained Horn Clauses to Software Verification
• Title（参考訳）: CHCのためのボトムアップ: 線形制約されたホーンクロースの新しいソフトウェア検証への変換
• Authors: Márk Somorjai, Mihály Dobos-Kovács, Zsófia Ádám, Levente Bajczi, András Vörös,
• Abstract要約: 制約付きホーンクロース(CHC)は、従来、形式的検証において低レベルな表現として用いられてきた。 線形CHCに対する別のボトムアップ手法を提案し、オープンソースのモデルチェックフレームワーク THETA における2つの選択肢を評価する。
• 参考スコア（独自算出の注目度）: 0.09786690381850355
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Constrained Horn Clauses (CHCs) have conventionally been used as a low-level representation in formal verification. Most existing solvers use a diverse set of specialized techniques, including direct state space traversal or under-approximating abstraction, necessitating purpose-built complex algorithms. Other solvers successfully simplified the verification workflow by translating the problem to inputs for other verification tasks, leveraging the strengths of existing algorithms. One such approach transforms the CHC problem into a recursive program roughly emulating a top-down solver for the deduction task; and verifying the reachability of a safety violation specified as a control location. We propose an alternative bottom-up approach for linear CHCs, and evaluate the two options in the open-source model checking framework THETA on both synthetic and industrial examples. We find that there is a more than twofold increase in the number of solved tasks when the novel bottom-up approach is used in the verification workflow, in contrast with the top-down technique.
• Abstract（参考訳）: 制約付きホーンクロース(CHC)は、従来、形式的検証において低レベルな表現として用いられてきた。 既存の問題解決者は、直接状態空間トラバーサルや非近似抽象、目的に構築された複雑なアルゴリズムを必要とするなど、様々な特殊技術を使っている。 他の解決者は、既存のアルゴリズムの強みを利用して、問題を他の検証タスクの入力に翻訳することで、検証ワークフローをシンプルにしました。 このようなアプローチの1つは、CHC問題を、推論タスクのトップダウン解決器を大まかにエミュレートした再帰プログラムに変換し、制御位置として指定された安全違反の到達可能性を検証する。 本稿では,線形CHCに対する新たなボトムアップ手法を提案し,オープンソースモデルチェックフレームワーク THETA における2つの選択肢を,合成例と工業例の両方で評価する。 トップダウン手法とは対照的に,新たなボトムアップ手法が検証ワークフローで使用される場合,解決タスク数が2倍以上に増加することが判明した。

関連論文リスト

• CoSIGN: Few-Step Guidance of ConSIstency Model to Solve General INverse Problems [3.3969056208620128]
  我々は, 高い復元品質を維持しつつ, 推論ステップの境界を1-2 NFEに推し進めることを提案する。 本手法は拡散型逆問題解法における新しい最先端技術を実現する。
  論文  参考訳（メタデータ） (2024-07-17T15:57:50Z)
• Weakly Supervised Co-training with Swapping Assignments for Semantic Segmentation [21.345548821276097]
  クラスアクティベーションマップ(CAM)は通常、擬似ラベルを生成するために弱教師付きセマンティックセマンティックセグメンテーション(WSSS)で使用される。 我々は、ガイド付きCAMを組み込んだエンドツーエンドWSSSモデルを提案し、CAMをオンラインで同時最適化しながらセグメンテーションモデルを訓練する。 CoSAは、追加の監督を持つものを含む、既存のマルチステージメソッドをすべて上回る、最初のシングルステージアプローチである。
  論文  参考訳（メタデータ） (2024-02-27T21:08:23Z)
• FlowPG: Action-constrained Policy Gradient with Normalizing Flows [14.98383953401637]
  ACRL(Action-Constrained reinforcement learning)は、安全クリティカルなリソース関連意思決定問題を解決するための一般的な手法である。 ACRLの最大の課題は、各ステップにおける制約を満たす有効なアクションを取るエージェントを確保することである。
  論文  参考訳（メタデータ） (2024-02-07T11:11:46Z)
• PSDiff: Diffusion Model for Person Search with Iterative and Collaborative Refinement [59.6260680005195]
  本稿では,拡散モデルであるPSDiffに基づく新しいPerson Searchフレームワークを提案する。 PSDiffは、ノイズの多いボックスとReID埋め込みから地上の真実へのデュアルデノケーションプロセスとして検索する人を定式化する。 新しいパラダイムに従って、我々は、反復的かつ協調的な方法で検出とReIDサブタスクを最適化する新しいコラボレーティブ・デノナイジング・レイヤ(CDL)を設計する。
  論文  参考訳（メタデータ） (2023-09-20T08:16:39Z)
• Small Object Detection via Coarse-to-fine Proposal Generation and Imitation Learning [52.06176253457522]
  本稿では,粗粒度パイプラインと特徴模倣学習に基づく小型物体検出に適した2段階フレームワークを提案する。 CFINetは、大規模な小さなオブジェクト検出ベンチマークであるSODA-DとSODA-Aで最先端の性能を達成する。
  論文  参考訳（メタデータ） (2023-08-18T13:13:09Z)
• Q-SHED: Distributed Optimization at the Edge via Hessian Eigenvectors Quantization [5.404315085380945]
  ニュートン型(NT)法は、DO問題における堅牢な収束率の実現要因として提唱されている。 インクリメンタルなヘッセン固有ベクトル量子化に基づく新しいビット割り当て方式を特徴とする、DOのための元のNTアルゴリズムであるQ-SHEDを提案する。 Q-SHEDはコンバージェンスに必要な通信ラウンド数を最大60%削減できることを示す。
  論文  参考訳（メタデータ） (2023-05-18T10:15:03Z)
• Efficient Alternating Minimization Solvers for Wyner Multi-View Unsupervised Learning [0.0]
  本稿では,計算効率のよい解法の開発を可能にする2つの新しい定式化法を提案する。 提案した解法は, 計算効率, 理論的収束保証, ビュー数による局所最小値複雑性, 最先端技術と比較して, 例外的な精度を提供する。
  論文  参考訳（メタデータ） (2023-03-28T10:17:51Z)
• MARLIN: Soft Actor-Critic based Reinforcement Learning for Congestion Control in Real Networks [63.24965775030673]
  そこで本研究では,汎用的な渋滞制御(CC)アルゴリズムを設計するための新しい強化学習(RL)手法を提案する。 我々の解であるMARLINは、Soft Actor-Criticアルゴリズムを用いてエントロピーとリターンの両方を最大化する。 我々は,MARLINを実ネットワーク上で訓練し,実ミスマッチを克服した。
  論文  参考訳（メタデータ） (2023-02-02T18:27:20Z)
• General Cutting Planes for Bound-Propagation-Based Neural Network Verification [144.7290035694459]
  任意の切削平面制約を加えることができるような境界伝搬手順を一般化する。 MIPソルバは、境界プロパゲーションベースの検証器を強化するために高品質な切削面を生成することができる。 本手法は,oval20ベンチマークを完全解き,oval21ベンチマークの2倍のインスタンスを検証できる最初の検証器である。
  論文  参考訳（メタデータ） (2022-08-11T10:31:28Z)
• ReAct: Temporal Action Detection with Relational Queries [84.76646044604055]
  本研究は,アクションクエリを備えたエンコーダ・デコーダフレームワークを用いて,時間的行動検出(TAD)の進展を図ることを目的とする。 まず,デコーダ内の関係注意機構を提案し,その関係に基づいてクエリ間の関心を誘導する。 最後に、高品質なクエリを区別するために、推論時に各アクションクエリのローカライズ品質を予測することを提案する。
  論文  参考訳（メタデータ） (2022-07-14T17:46:37Z)
• Combining Deep Learning and Optimization for Security-Constrained Optimal Power Flow [94.24763814458686]
  セキュリティに制約のある最適電力フロー(SCOPF)は、電力システムの基本である。 SCOPF問題におけるAPRのモデル化は、複雑な大規模混合整数プログラムをもたらす。 本稿では,ディープラーニングとロバスト最適化を組み合わせた新しい手法を提案する。
  論文  参考訳（メタデータ） (2020-07-14T12:38:21Z)

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

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