論文の概要: Hyper model checking for high-level relational models

• arxiv url: http://arxiv.org/abs/2512.12024v1
• Date: Fri, 12 Dec 2025 20:30:41 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-12-16 17:54:56.077482
• Title: Hyper model checking for high-level relational models
• Title（参考訳）: 高次関係モデルに対するハイパーモデルチェック
• Authors: Nuno Macedo, Hugo Pacheco,
• Abstract要約: そこで本研究では,Pardinusを拡張し,関係モデル上でのハイパープロパティの自動検証を行う新しいモデル探索手法を提案する。 その後、アロイを保守的に拡張し、設計モデルに対する超正当性の仕様と自動検証をサポートする。
• 参考スコア（独自算出の注目度）: 1.2400116527089995
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Many properties related to security or concurrency must be encoded as so-called hyperproperties, temporal properties that allow reasoning about multiple traces of a system. However, despite recent advances on model checking hyperproperties, there is still a lack of higher-level specification languages that can effectively support software engineering practitioners in verifying properties of this class at early stages of system design. Alloy is a lightweight formal method with a high-level specification language that is supported by automated analysis procedures, making it particularly well-suited for the verification of design models at early development stages. It does not natively support, however, the verification of hyperproperties. This work proposes HyperPardinus, a new model finding procedure that extends Pardinus -- the temporal logic backend of the Alloy language -- to automatically verify hyperproperties over relational models by relying on existing low-level model checkers for hyperproperties. It then conservatively extends Alloy to support the specification and automatic verification of hyperproperties over design models, as well as the visualization of (counter-)examples at a higher-level of abstraction. Evaluation shows that our approach enables modeling and finding (counter-)examples for complex hyperproperties with alternating quantifiers, making it feasible to address relevant scenarios from the state of the art.
• Abstract（参考訳）: セキュリティや並行性に関連する多くのプロパティは、システムの複数のトレースに関する推論を可能にする、いわゆる超越性(hyperproperties)としてエンコードされなければならない。 しかし、モデルチェックハイパープロパティの最近の進歩にもかかわらず、システム設計の初期段階において、このクラスの特性を検証する際に、ソフトウェア工学の実践者を効果的にサポートできる高レベルな仕様言語はいまだに存在しない。 Alloyは、高度な仕様言語を備えた軽量な形式的手法であり、自動解析によってサポートされており、特に初期の開発段階での設計モデルの検証に適している。 しかし、ハイパープロパティの検証をネイティブにサポートしていない。 この研究は、アロイ言語の時間論理バックエンドであるPardinusを拡張した新しいモデル発見手順であるHyperPardinusを提案し、既存の低レベルのモデルチェッカーをハイパープロパティに頼って、リレーショナルモデル上のハイパープロパティを自動的に検証する。 その後、アロイを保守的に拡張し、設計モデルに対するハイパープロパティの仕様と自動検証をサポートし、高レベルの抽象化で(カウンタ-)サンプルを視覚化する。 評価の結果,提案手法は複雑な超正則のモデリングと(対数)例を交互に行うことが可能であり,最先端技術から関連するシナリオに対処することが可能であることがわかった。

関連論文リスト

• Retrieval-augmented reasoning with lean language models [5.615564811138556]
  複雑なドメイン固有のクエリを解釈できる検索拡張会話エージェントを開発した。 本システムでは,細調整されたQwen2.5-Instructモデルと高密度レトリバーを統合した。 すべての実装の詳細とコードは、ドメイン間のサポートと適応のために公開されています。
  論文  参考訳（メタデータ） (2025-08-15T10:38:15Z)
• Sequential-Parallel Duality in Prefix Scannable Models [68.39855814099997]
  近年では Gated Linear Attention (GLA) や Mamba など様々なモデルが開発されている。 ニアコンスタント時間並列評価と線形時間、定数空間シーケンシャル推論をサポートするニューラルネットワークモデルの全クラスを特徴付けることができるだろうか?
  論文  参考訳（メタデータ） (2025-06-12T17:32:02Z)
• COrAL: Order-Agnostic Language Modeling for Efficient Iterative Refinement [80.18490952057125]
  反復改良は、複雑なタスクにおける大規模言語モデル(LLM)の能力を高める効果的なパラダイムとして登場した。 我々はこれらの課題を克服するために、コンテキストワイズ順序非依存言語モデリング(COrAL)を提案する。 当社のアプローチでは、管理可能なコンテキストウィンドウ内で複数のトークン依存関係をモデル化しています。
  論文  参考訳（メタデータ） (2024-10-12T23:56:19Z)
• Runtime Verification on Abstract Finite State Models [0.0]
  マルチスレッドJavaプログラムの実行から有限状態モデルを抽出する方法を示し、精度特性のランタイム検証を実行する。 本論文の主な貢献は,プロパティ保存抽象モデルのオンラインプロパティチェックを通じて,実行時検証の効率性を示すことである。
  論文  参考訳（メタデータ） (2024-06-18T15:32:31Z)
• SemPat: Using Hyperproperty-based Semantic Analysis to Generate Microarchitectural Attack Patterns [4.4182738040054685]
  ソフトウェアのマイクロアーキテクチャのセキュリティ検証には2つの幅広いアプローチがある。 1つ目は、特定のプログラムとハードウェアマイクロアーキテクチャの特定の抽象モデルに対して検証されるセマンティックセキュリティ特性に基づいている。 2つ目は攻撃パターンに基づいており、プログラムの実行で見つかった場合、エクスプロイトの存在を示す。
  論文  参考訳（メタデータ） (2024-06-08T08:54:27Z)
• GrootVL: Tree Topology is All You Need in State Space Model [66.36757400689281]
  GrootVLは、視覚的タスクとテキストタスクの両方に適用できる多目的マルチモーダルフレームワークである。 本手法は, 画像分類, オブジェクト検出, セグメンテーションにおいて, 既存の構造化状態空間モデルよりも大幅に優れる。 大規模言語モデルの微調整により,本手法は訓練コストの少ない複数のテキストタスクにおいて一貫した改善を実現する。
  論文  参考訳（メタデータ） (2024-06-04T15:09:29Z)
• Tracing Hyperparameter Dependencies for Model Parsing via Learnable Graph Pooling Network [21.484648648511854]
  本稿では,LGPN(Learningable Graph Pooling Network)と呼ばれる新しいモデル解析手法を提案する。 LGPNには、モデル解析に適した学習可能なプールアンプール機構が組み込まれている。 提案手法をCNN生成画像検出と協調攻撃検出に拡張する。
  論文  参考訳（メタデータ） (2023-12-03T22:05:05Z)
• Generalization Properties of Retrieval-based Models [50.35325326050263]
  検索ベースの機械学習手法は、幅広い問題で成功をおさめた。 これらのモデルの約束を示す文献が増えているにもかかわらず、そのようなモデルの理論的基盤はいまだに解明されていない。 本稿では,その一般化能力を特徴付けるために,検索ベースモデルの形式的処理を行う。
  論文  参考訳（メタデータ） (2022-10-06T00:33:01Z)
• Parameterized Hypercomplex Graph Neural Networks for Graph Classification [1.1852406625172216]
  我々は超複雑特徴変換の特性を利用するグラフニューラルネットワークを開発した。 特に、提案したモデルのクラスでは、代数自身を特定する乗法則は、トレーニング中にデータから推測される。 提案するハイパーコンプレックスgnnをいくつかのオープングラフベンチマークデータセット上でテストし,そのモデルが最先端の性能に達することを示す。
  論文  参考訳（メタデータ） (2021-03-30T18:01:06Z)
• DirectDebug: Automated Testing and Debugging of Feature Models [55.41644538483948]
  変数モデル(例えば、特徴モデル)は、ソフトウェアアーティファクトの変数と共通性を表現する一般的な方法である。 複雑でしばしば大規模な機能モデルは欠陥になりうる、すなわち、ソフトウェアアーチファクトの期待される変動特性を表現しない。
  論文  参考訳（メタデータ） (2021-02-11T11:22:20Z)
• Automated and Formal Synthesis of Neural Barrier Certificates for Dynamical Models [70.70479436076238]
  バリア証明書(BC)の自動的,形式的,反例に基づく合成手法を提案する。 このアプローチは、ニューラルネットワークとして構造化されたBCの候補を操作する誘導的フレームワークと、その候補の有効性を認証するか、反例を生成する音検証器によって支えられている。 その結果,音のBCsを最大2桁の速度で合成できることがわかった。
  論文  参考訳（メタデータ） (2020-07-07T07:39:42Z)

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

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