論文の概要: HyperQB: A Bounded Model Checker for Hyperproperties

• arxiv url: http://arxiv.org/abs/2109.12989v6
• Date: Tue, 21 Oct 2025 16:25:55 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-11-01 03:08:28.056642
• Title: HyperQB: A Bounded Model Checker for Hyperproperties
• Title（参考訳）: HyperQB:Hyperpropertiesのバウンドモデルチェッカー
• Authors: Tzu-Han Hsu, Milad Rabizadeh, Kenneth Rogale, Fedor Filippov, Marco A. de Oliveira Batista, César Sánchez, Borzoo Bonakdarpour,
• Abstract要約: HyperQB 2.0は、ハイパープロパティのための最初の高効率なプッシュボタンバウンドモデルチェッカー(BMC)である。 NuSMV や Verilog のモデルとして入力され、時相論理の HyperLTL や A-HLTL で表される式である。 このツールはRustで完全に実装されています。
• 参考スコア（独自算出の注目度）: 2.0580394963474453
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We introduce the tool HyperQB 2.0, the first highly efficient push-button bounded model checker (BMC) for hyperproperties. HyperQB takes as input a model in NuSMV or Verilog and a formula expressed in the temporal logics HyperLTL or A-HLTL. The core decision procedures to implement BMC are SMT and QBF solvers, enabling verification of finite- and infinite-state programs. HyperQB offers command-line and standalone graphical, and web-based interfaces. Based on the selection of either bug-hunting or synthesis, instances of counterexamples or path witnesses are returned. The tool is entirely implemented in Rust and we report on successful and effective model checking results for a rich set of experiments on a variety of case studies with rigorous performance comparison and contrast with similar tools.
• Abstract（参考訳）: 提案ツールであるHyperQB 2.0は,超高効率なプッシュボタン境界モデルチェッカー(BMC)である。 HyperQB は NuSMV や Verilog のモデルとして入力され、時相論理の HyperLTL や A-HLTL で表される式である。 BMCを実装するための中核的な決定手順は、有限状態および無限状態プログラムの検証を可能にするSMTとQBFソルバである。 HyperQBはコマンドラインとスタンドアロンのグラフィカルとWebベースのインターフェースを提供する。 バグハンティングまたは合成のいずれかの選択に基づいて、反例やパス目撃者のインスタンスが返される。 このツールはRustで完全に実装されており、厳密なパフォーマンス比較と類似のツールとの対比によるさまざまなケーススタディに関する豊富な実験に対して、成功した効果的なモデルチェック結果について報告します。

関連論文リスト

• MBTModelGenerator: A software tool for reverse engineering of Model-based Testing (MBT) models from clickstream data of web applications [1.516251872371896]
  このツールはUIイベントをキャプチャして状態遷移モデルに変換し、その結果をGraphWalker MBTツールと互換性のあるフォーマットでエクスポートする。 本報告では, システム要件, 設計決定, 実装詳細, テストプロセス, ツールの実証評価について報告する。
  論文  参考訳（メタデータ） (2025-06-09T19:44:10Z)
• Exploring Microstructural Dynamics in Cryptocurrency Limit Order Books: Better Inputs Matter More Than Stacking Another Hidden Layer [9.2463347238923]
  ニューラルネットワークに余分な隠蔽層やパラメータを追加することで、短期的な価格予測が真に向上するかどうかを検討することを目的としている。 我々は,BTC/USDT LOBスナップショットを100ミリ秒から複数秒間隔で公開して,解釈可能なベースライン,ロジスティック回帰,XGBoostからディープアーキテクチャ(DeepLOB,Conv1D+LSTM)まで,モデルをベンチマークする。
  論文  参考訳（メタデータ） (2025-06-06T05:43:30Z)
• Transformers for Complex Query Answering over Knowledge Hypergraphs [48.55646194244594]
  三重KGは、アーニティ2の実体と関係からなる古典的なKGとして、現実世界の事実の限定的な表現を持つ。 本稿では,2段階の変圧器モデルである論理知識ハイパーグラフ変換器(LKHGT)を提案する。 CQAデータセットの実験結果から,LKHGTはKHG上の最先端のCQA手法であり,アウト・オブ・ディストリビューションクエリタイプに一般化可能であることが示された。
  論文  参考訳（メタデータ） (2025-04-23T09:07:21Z)
• BPMN Analyzer 2.0: Instantaneous, Comprehensible, and Fixable Control Flow Analysis for Realistic BPMN Models [0.9903198600681908]
  デッドロックやライブロックのようなフローエラーを制御することは、ビジネスプロセスモデルの適切な実行を妨げる。 我々はBPMNモデルにおける制御フローエラーを瞬時に識別し、モデラーに理解できるようにし、修正を提案する新しいツールを紹介します。
  論文  参考訳（メタデータ） (2024-08-12T09:32:34Z)
• Instantaneous, Comprehensible, and Fixable Soundness Checking of Realistic BPMN Models [0.9903198600681908]
  私たちはBPMNモデルのエラーを瞬時に識別できる新しい音質チェックツールを導入しました。 ツールの音質チェックは,500ms未満の即時性であることを示す。 このツールはオープンソースで、モジュール化され、発見され、人気のあるBPMNモデリングツールに統合されています。
  論文  参考訳（メタデータ） (2024-07-04T14:34:52Z)
• Deductive Controller Synthesis for Probabilistic Hyperproperties [0.31317409221921133]
  本稿では,マルコフ決定過程(MDP)と確率的超越性(probabilistic hyperproperties)に対する制御器合成問題の解法を提案する。 我々のアプローチは、確率的超正則と追加の制御子内制約を効果的に組み合わせることのできる最初の手法である。
  論文  参考訳（メタデータ） (2023-07-10T11:55:44Z)
• CausalVLR: A Toolbox and Benchmark for Visual-Linguistic Causal Reasoning [107.81733977430517]
  CausalVLR(Causal Visual-Linguistic Reasoning)は、最先端の因果関係の発見と因果推論方法の豊富なセットを含むオープンソースのツールボックスである。 これらのメソッドはNVIDIAコンピューティングシステムの下でPyTorchを実装したツールボックスに含まれている。
  論文  参考訳（メタデータ） (2023-06-30T08:17:38Z)
• Dissecting Multimodality in VideoQA Transformer Models by Impairing Modality Fusion [54.33764537135906]
  VideoQA Transformerモデルは標準ベンチマークで競合性能を示す。 これらのモデルはビデオとテキストからリッチなマルチモーダル構造とダイナミックスを一緒に捉えていますか? 彼らはバイアスと刺激的な特徴を利用して高いスコアを達成していますか?
  論文  参考訳（メタデータ） (2023-06-15T06:45:46Z)
• Single-Stage Visual Relationship Learning using Conditional Queries [60.90880759475021]
  TraCQは、マルチタスク学習問題とエンティティペアの分布を回避する、シーングラフ生成の新しい定式化である。 我々は,DETRをベースとしたエンコーダ-デコーダ条件付きクエリを用いて,エンティティラベル空間を大幅に削減する。 実験結果から、TraCQは既存のシングルステージシーングラフ生成法よりも優れており、Visual Genomeデータセットの最先端の2段階メソッドを多く上回っていることがわかった。
  論文  参考訳（メタデータ） (2023-06-09T06:02:01Z)
• Bilaterally Slimmable Transformer for Elastic and Efficient Visual Question Answering [75.86788916930377]
  左右にスリム化可能なトランスフォーマー(BST)は任意のトランスフォーマーベースのVQAモデルに統合される。 1つのスリム化MCAN-BSTサブモデルは、VQA-v2で同等の精度を達成する。 最も小さなMCAN-BSTサブモデルは、推論中に9Mパラメータと0.16GのFLOPを持つ。
  論文  参考訳（メタデータ） (2022-03-24T02:26:04Z)

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

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