論文の概要: Syntax-driven Incremental Program Verification of Matching Logic Properties

• arxiv url: http://arxiv.org/abs/2606.08824v1
• Date: Sun, 07 Jun 2026 20:32:37 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-06-09 14:42:06.469215
• Title: Syntax-driven Incremental Program Verification of Matching Logic Properties
• Title（参考訳）: 構文駆動型増分プログラムによるマッチング論理特性の検証
• Authors: Domenico Bianculli, Antonio Filieri, Carlo Ghezzi, Dino Mandrioli, Alessandro Maria Rizzi,
• Abstract要約: 本稿では, KernelC で記述されたプログラムの漸進的な検証手法を提案する。 このアプローチは、コードチャンクを分離して分析できる構文意味論的なフレームワークに基づいている。 その結果,本手法は形式検証の効率を低下させず,変更後のプログラム再検証よりも優れていることがわかった。
• 参考スコア（独自算出の注目度）: 36.861969535480526
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Incrementality is a fundamental design principle to master the complexity of large, long-lived software systems. This principle has been embraced by agile development processes and it lays at the base of continuous software evolution. A major challenge in this context is to incrementally re-verify the correctness of software artifacts after every change, focusing the verification efforts only on the parts affected by the change. We present an approach to the incremental verification of programs written in KernelC, annotated with properties expressed in matching logic. The approach is based on a syntactic-semantic framework that enables analyzing code chunks in isolation so that, after a change to a program fragment, only the part whose semantics is affected by the change is re-processed. This property is obtained by expressing the language syntax through an operator precedence grammar and by formalizing its semantics through a synthesized attribute schema. We have implemented our technique in a prototype tool and experimentally evaluated its effectiveness. The results show that our approach does not penalize the efficiency of formal verification and can outperform program re-verification after changes, depending on the presence and type of annotations, as well as the position of the change and the program structure.
• Abstract（参考訳）: インクリメンタリティは、大規模で長期間のソフトウェアシステムの複雑さをマスターする基本的な設計原則である。 この原則はアジャイル開発プロセスによって受け入れられ、継続的ソフトウェア進化の基盤に置かれています。 この文脈における大きな課題は、変更毎にソフトウェアアーチファクトの正しさを段階的に再検証し、変更によって影響を受ける部分のみに検証の取り組みを集中させることです。 本稿では,KernelCで記述されたプログラムに,マッチングロジックで表現された属性を付加した漸進的な検証手法を提案する。 プログラムフラグメントの変更後、その変更によって意味が影響を受ける部分のみが再処理されるように、コードのチャンクを分離して分析できる構文・セマンティックフレームワークに基づいている。 この特性は、演算子優先文法で言語構文を表現し、合成属性スキーマでその意味を定式化することによって得られる。 本手法を試作ツールに実装し,その有効性を実験的に評価した。 その結果,提案手法は形式的検証の効率を低下させるものではなく,アノテーションの存在や型,変更位置やプログラム構造に応じて,変更後のプログラム再検証よりも優れていることがわかった。

関連論文リスト

• AlgoTouch: An Execution-Centered Approach to Incremental Construction of Imperative Programs [0.0]
  AlgoTouchは命令型プログラムをインクリメンタルに構築するための実行ベースのシステムである。 データストレージ、計算、制御フローを公開する明示的な記法機械に依存している。 AlgoTouchはPython、C、C++、Javaで正しい読みやすいプログラムを自動的に生成する。
  論文  参考訳（メタデータ） (2026-06-02T08:57:49Z)
• What Really Improves Mathematical Reasoning: Structured Reasoning Signals Beyond Pure Code [72.9921566968371]
  ドメイン分離のきめ細かい10T-tokenコーパスにおける事前学習の制御実験により,コードが推論を改善するという主張を再考する。 コードはプログラミング能力を大幅に改善するが、一般的な推論エンハンサーとして機能しない。 コード-テキストと数学-テキストの混合のようなドメイン間構造的推論トレースがよりうまく説明されている。
  論文  参考訳（メタデータ） (2026-05-19T12:37:01Z)
• Governed Metaprogramming for Intelligent Systems: Reclassifying Eval as a Governed Effect [0.0]
  プログラム表現が第一級値となる言語設計であるメタプログラミングについて述べる。 形式操作の純粋性、非バイパス定理、境界保存の3つの性質を証明している。 中心的な貢献は、evalを言語プリミティブから支配的なエフェクトに再分類することである。
  論文  参考訳（メタデータ） (2026-05-05T02:56:43Z)
• Multi-Agent Procedural Graph Extraction with Structural and Logical Refinement [66.51979814832332]
  モデル式は、専用の構造的および論理的洗練を伴う多ラウンド推論プロセスとして手続きグラフ抽出を定式化する。 実験により、モデルが強いベースラインに対して構造的正当性と論理的整合性の両方において大幅に改善されることが示されている。
  論文  参考訳（メタデータ） (2026-01-27T04:00:48Z)
• Accelerate Speculative Decoding with Sparse Computation in Verification [49.74839681322316]
  投機的復号化は、複数のドラフトトークンを並列に検証することにより、自動回帰言語モデル推論を加速する。 既存のスペーシフィケーション方式は主にトークン・バイ・トーケンの自己回帰復号化のために設計されている。 そこで本研究では,注目度,FFN,MoEを両立させるスパース検証フレームワークを提案する。
  論文  参考訳（メタデータ） (2025-12-26T07:53:41Z)
• How Different Tokenization Algorithms Impact LLMs and Transformer Models for Binary Code Analysis [0.0]
  その重要性にもかかわらず、アセンブリコードのコンテキストにおけるトークン化は未探索領域のままである。 我々は、アセンブリコードのユニークな特徴に合わせて、プリプロセスのカスタマイズオプションとプリトークン化ルールについて検討する。 我々は,トークン化効率,語彙圧縮,組立符号の表現忠実度に基づくトークン化器の比較を行った。
  論文  参考訳（メタデータ） (2025-11-05T19:45:26Z)
• Autoformalizer with Tool Feedback [52.334957386319864]
  自動形式化は、数学的問題を自然言語から形式的ステートメントに変換することによって、ATP(Automated Theorem Proving)のデータ不足に対処する。 既存のフォーミュラライザは、構文的妥当性とセマンティック一貫性を満たす有効なステートメントを一貫して生成することに苦慮している。 本稿では,ツールフィードバックを用いたオートフォーマライザ (ATF) を提案する。
  論文  参考訳（メタデータ） (2025-10-08T10:25:12Z)
• Inferring Attributed Grammars from Parser Implementations [1.0217990949413291]
  本稿では,入力文法の実装から属性文法を推定する新しい手法を提案する。 実行時の実行を観察し,プログラムの振る舞いを文法にマッピングすることにより,文法規則に意味的アクションを体系的に抽出し,組み込む。 プログラムの初期セットを用いて,提案手法の有効性を実証し,生成した属性文法を用いてプログラムの動作を正確に再現可能であることを示す。
  論文  参考訳（メタデータ） (2025-07-17T13:32:59Z)
• Enforcing Consistency in Weakly Supervised Semantic Parsing [68.2211621631765]
  本稿では,関連する入力に対する出力プログラム間の整合性を利用して,スプリアスプログラムの影響を低減することを提案する。 より一貫性のあるフォーマリズムは、一貫性に基づくトレーニングを必要とせずに、モデルパフォーマンスを改善することにつながります。
  論文  参考訳（メタデータ） (2021-07-13T03:48:04Z)

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

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