論文の概要: Tractable Verification of Model Transformations: A Cutoff-Theorem Approach for DSLTrans
- arxiv url: http://arxiv.org/abs/2604.18792v2
- Date: Thu, 23 Apr 2026 12:23:22 GMT
- ステータス: 翻訳完了
- システム内更新日: 2026-04-24 14:40:06.025417
- Title: Tractable Verification of Model Transformations: A Cutoff-Theorem Approach for DSLTrans
- Title（参考訳）: モデル変換のトラクタブル検証:DSLTransのためのカットオフ理論アプローチ
- Authors: Levi Lucio,
- Abstract要約: DSLTransは、検証性を改善するためにチューリング不完全であるように設計された。
本稿では、DSLTransのための抽出可能な検証ワークフローを提示し、完了時に形式化する。
- 参考スコア（独自算出の注目度）: 0.0
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Model transformations are central to MDE, but formal verification is difficult because mainstream transformation languages are undecidable. DSLTrans was designed to be Turing-incomplete to improve verifiability, yet earlier verification based on path-condition enumeration still suffered exponential blow-up and did not scale to realistic cases. We present a tractable verification workflow for DSLTrans and formalize when it is complete. The method combines three contributions: (i) a Cutoff Theorem proving that bounded model checking is complete for a precise DSLTrans fragment and positive existence/traceability properties, turning an infinite search into a finite computable bound; (ii) composable, soundness-preserving optimizations (per-class bounds, CEGAR-based fragment verification, and trace-aware dependency analysis) that reduce SMT encoding size; and (iii) a Z3-based implementation evaluated on realistic transformations from the ATL Zoo and related benchmarks. On 29 concrete transformations and 899 properties spanning compiler lowering, schema translation, behavioral modeling, graph mapping, and stress tests, 552 properties are proved, 345 produce concrete counterexamples (including intentional negative and boundary cases), and only 2 remain undecided within timeout. For properties beyond the tractability budget, we introduce tractability-driven refinement (precondition specialization, postcondition decomposition, and transformation instrumentation), achieving up to 112x speedup while eliminating spurious counterexamples. The workflow is supported by a web IDE and a concrete execution engine for runtime validation.
- Abstract（参考訳）: モデル変換はMDEの中心であるが、主流の変換言語は決定不可能であるため、形式的な検証は難しい。
DSLTransは、検証性を改善するためにチューリング不完全として設計されたが、パス条件列挙に基づく早期検証はまだ急激な爆発を経験しており、現実的なケースには拡張できなかった。
本稿では、DSLTransのための抽出可能な検証ワークフローを提示し、完了時に形式化する。
この方法は3つのコントリビューションを結合する。
(i) 有界モデル検査が正確なDSLTransフラグメントと正の存在/追跡性特性に対して完全であることを証明したカットオフ定理により、無限探索を有限計算可能な有界に変換する。
(ii)SMT符号化サイズを小さくする構成可能、音質保存最適化(クラス別境界、CEGARによるフラグメント検証、トレース対応依存性分析)
(iii) ATL Zooと関連するベンチマークから現実的な変換を評価するZ3ベースの実装。
29の具体的な変換と899のプロパティがコンパイラの低下、スキーマ変換、行動モデリング、グラフマッピング、ストレステストにまたがって、52のプロパティが証明された。
トラクタビリティ予算を超越した特性に対しては,トラクタビリティ改善(プレコンディショナライゼーション,ポストコンディション分解,トランスフォーメーションインスツルメンテーション)を導入し,最大112倍の高速化を実現し,突発的な反例を排除した。
ワークフローは、Web IDEとランタイムバリデーションのための具体的な実行エンジンによってサポートされている。
関連論文リスト
- Towards Counterfactual Explanation and Assertion Inference for CPS Debugging [0.0]
本稿では,サイバー物理システムのための実証的説明とアサーションに基づくキャラクタリゼーションフレームワークであるDeCaFを紹介する。
テスト入力がフェールすると、DeCaFは入力信号の反ファクト変化を生成し、テストが通過しないよう変換する。
提案手法は,3つの反事実生成器と2つの因果モデルを組み合わせて,成功の主張を推測する。
論文 参考訳（メタデータ） (2026-04-09T00:53:00Z) - Dynamic analysis enhances issue resolution [53.50448142467294]
DAIRA(Dynamic Analysis-enhanced Issue Resolution Agent)は、エージェントの推論サイクルに動的解析を組み込む自動修復フレームワークである。
テストトレース駆動の方法論によって駆動されるDAIRAは、軽量モニタを使用して重要なランタイムデータを抽出する。
Gemini 3 Flash Previewを使用すると、DAIRAは新たな最先端(SOTA)パフォーマンスを確立し、SWE-bench Verifiedデータセットで79.4%の解像度を達成する。
論文 参考訳（メタデータ） (2026-03-23T14:48:54Z) - Veri-Sure: A Contract-Aware Multi-Agent Framework with Temporal Tracing and Formal Verification for Correct RTL Code Generation [4.723302382132762]
シリコングレードの正しさは、 (i) シミュレーション中心の評価の限られたカバレッジと信頼性、 (ii) 回帰と修復幻覚、 (iii) エージェントハンドオフ間で意図が再解釈される意味的ドリフトによってボトルネックが残っている。
エージェントの意図を整合させる設計契約を確立するマルチエージェントフレームワークであるVeri-Sureを提案する。
論文 参考訳（メタデータ） (2026-01-27T16:10:23Z) - You Only Need Your Transformer 25% of the Time: Meaning-First Execution for Eliminating Unnecessary Inference [0.0]
本稿では,このフレームワークを実装したコントロールプレーンアーキテクチャであるMeaning-First Execution (MFEE)を紹介する。
MFEEは78.1%の実行削減を実現し、呼び出された実行に対する100%の正確なマッチ等価性を維持している。
論文 参考訳（メタデータ） (2025-12-29T08:03:52Z) - Theoretical Foundations of Prompt Engineering: From Heuristics to Expressivity [0.0]
本研究では,トランスフォーマーのバックボーンをエグゼキュータとして固定し,プロンプトのみを変化させることで得られる機能群について検討する。
一つの固定されたバックボーンがプロンプトだけで対象の行動の幅広いクラスを近似できることを示す。
論文 参考訳（メタデータ） (2025-12-14T13:42:20Z) - Formal that "Floats" High: Formal Verification of Floating Point Arithmetic [0.0]
本稿では,金の基準モデルに対する直接RTL-RTLモデルによる浮動小数点演算の検証方法を提案する。
この方法論はエージェントAIベースの形式的プロパティ生成によって拡張され、大規模言語モデル(LLM)駆動の自動化とHuman-in-the-Loop(HITL)の洗練を統合する。
その結果, RTL-to-RTLモデルの直接チェックは, 適用効率が向上し, スタンドアロンの検証よりもアサーションが少なくなることがわかった。
論文 参考訳（メタデータ） (2025-12-07T14:03:44Z) - Autoformalizer with Tool Feedback [52.334957386319864]
自動形式化は、数学的問題を自然言語から形式的ステートメントに変換することによって、ATP(Automated Theorem Proving)のデータ不足に対処する。
既存のフォーミュラライザは、構文的妥当性とセマンティック一貫性を満たす有効なステートメントを一貫して生成することに苦慮している。
本稿では,ツールフィードバックを用いたオートフォーマライザ (ATF) を提案する。
論文 参考訳（メタデータ） (2025-10-08T10:25:12Z) - COrAL: Order-Agnostic Language Modeling for Efficient Iterative Refinement [80.18490952057125]
反復改良は、複雑なタスクにおける大規模言語モデル(LLM)の能力を高める効果的なパラダイムとして登場した。
我々はこれらの課題を克服するために、コンテキストワイズ順序非依存言語モデリング(COrAL)を提案する。
当社のアプローチでは、管理可能なコンテキストウィンドウ内で複数のトークン依存関係をモデル化しています。
論文 参考訳（メタデータ） (2024-10-12T23:56:19Z) - A Template-based Method for Constrained Neural Machine Translation [100.02590022551718]
本稿では,デコード速度を維持しつつ,高い翻訳品質と精度で結果が得られるテンプレートベースの手法を提案する。
テンプレートの生成と導出は、1つのシーケンスからシーケンスまでのトレーニングフレームワークを通じて学習することができる。
実験結果から,提案手法は語彙的,構造的に制約された翻訳タスクにおいて,いくつかの代表的ベースラインを上回り得ることが示された。
論文 参考訳（メタデータ） (2022-05-23T12:24:34Z) - CoCoMoT: Conformance Checking of Multi-Perspective Processes via SMT
(Extended Version) [62.96267257163426]
我々はCoCoMoT(Computing Conformance Modulo Theories)フレームワークを紹介する。
まず、純粋な制御フロー設定で研究したSATベースのエンコーディングを、データ認識ケースに持ち上げる方法を示す。
次に,プロパティ保存型クラスタリングの概念に基づく新しい前処理手法を提案する。
論文 参考訳（メタデータ） (2021-03-18T20:22:50Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。