論文の概要: Automatic Program Instrumentation for Automatic Verification (Extended Technical Report)

• arxiv url: http://arxiv.org/abs/2306.00004v1
• Date: Fri, 26 May 2023 14:55:35 GMT
• ステータス: 処理完了
• システム内更新日: 2023-10-24 04:56:37.721755
• Title: Automatic Program Instrumentation for Automatic Verification (Extended Technical Report)
• Title（参考訳）: 自動検証のための自動プログラムインスツルメンテーション(拡張技術報告)
• Authors: Jesper Amilon, Zafer Esen, Dilian Gurov, Christian Lidstr\"om, Philipp R\"ummer
• Abstract要約: 帰納的検証とソフトウェアモデルチェックでは、特定の仕様言語構造を扱うことが問題となる。 本稿では,様々なアドホックなアプローチを仮定する統一検証パラダイムとして,インスツルメンテーションを提案する。 我々は,プログラムのアグリゲーションによる検証に適したMonoCeraツールにアプローチを実装した。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: In deductive verification and software model checking, dealing with certain specification language constructs can be problematic when the back-end solver is not sufficiently powerful or lacks the required theories. One way to deal with this is to transform, for verification purposes, the program to an equivalent one not using the problematic constructs, and to reason about its correctness instead. In this paper, we propose instrumentation as a unifying verification paradigm that subsumes various existing ad-hoc approaches, has a clear formal correctness criterion, can be applied automatically, and can transfer back witnesses and counterexamples. We illustrate our approach on the automated verification of programs that involve quantification and aggregation operations over arrays, such as the maximum value or sum of the elements in a given segment of the array, which are known to be difficult to reason about automatically. We formalise array aggregation operations as monoid homomorphisms. We implement our approach in the MonoCera tool, which is tailored to the verification of programs with aggregation, and evaluate it on example programs, including SV-COMP programs.
• Abstract（参考訳）: 帰納的検証とソフトウェアモデル検証では、バックエンドソルバが十分に強力でない場合や必要な理論が欠如している場合、特定の仕様言語構造を扱うことが問題となる。 この問題に対処する方法の1つは、検証のために、プログラムが問題のある構成物を使用しない同等のプログラムに変換し、代わりにその正しさを推論することである。 本稿では,既存の様々なアドホックアプローチを仮定し,明確な形式的正当性基準を持ち,自動的に適用でき,目撃者や反例を転送できる統一検証パラダイムとしての計測手法を提案する。 本稿では,配列上での定量化と集約処理を含むプログラムの自動検証について述べる。例えば,配列の各セグメントの要素の最大値や総和は,自動推論が困難であることが知られている。 配列アグリゲーション演算をモノイド準同型として定式化する。 本手法は,プログラムのアグリゲーションによる検証に適したMonoCeraツールに実装し,SV-COMPプログラムを含むサンプルプログラムで評価する。

関連論文リスト

• Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
  大規模言語モデル(LLM)は一貫性と正確な推論に苦しむ。 LLMは、主に正しいソリューションに基づいて訓練され、エラーを検出して学習する能力を減らす。 本稿では,CoT(Chain-of-Thought)とPoT(Program-of-Thought)を組み合わせた新しい協調手法を提案する。
  論文  参考訳（メタデータ） (2024-10-05T05:21:48Z)
• Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages [6.0608817611709735]
  本稿では,検証対応言語における仕様の質を評価するための指標を提案する。 MBPPコード生成ベンチマークのDafny仕様の人間ラベル付きデータセットに,我々の測定値が密接に一致することを示す。 また、このテクニックをより広く適用するために対処する必要がある正式な検証課題についても概説する。
  論文  参考訳（メタデータ） (2024-06-14T06:52:08Z)
• Prompt Optimization with EASE? Efficient Ordering-aware Automated Selection of Exemplars [66.823588073584]
  大規模言語モデル(LLM)は、現実世界のアプリケーションで印象的な機能を示している。 これらの卓越した作品の品質は、パフォーマンスに大きな影響を与えます。 既存の方法は、先行注文がパフォーマンスに与える影響を適切に説明できない。
  論文  参考訳（メタデータ） (2024-05-25T08:23:05Z)
• Bisimulation Learning [55.859538562698496]
  我々は、大きな、潜在的に無限の状態空間を持つ状態遷移系の有限バイシミュレートを計算する。 提案手法は,実際に行われている他の最先端ツールよりも高速な検証結果が得られる。
  論文  参考訳（メタデータ） (2024-05-24T17:11:27Z)
• Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification [15.686651364655958]
  AutoSpecは、自動プログラム検証のための仕様を合成するための自動化アプローチである。 仕様の汎用性における既存の作業の欠点を克服し、完全な証明のために十分かつ適切な仕様を合成する。 実世界のX509パーサプロジェクトでプログラムを検証するためにうまく適用することができる。
  論文  参考訳（メタデータ） (2024-03-31T18:15:49Z)
• Quantitative Assurance and Synthesis of Controllers from Activity Diagrams [4.419843514606336]
  確率的モデル検査は、定性的および定量的な性質を自動検証するために広く用いられている形式的検証手法である。 これにより、必要な知識を持っていない研究者やエンジニアにはアクセスできない。 本稿では,確率時間の新しいプロファイル,品質アノテーション,3つのマルコフモデルにおけるADの意味論的解釈,アクティビティ図からPRISM言語への変換ルールのセットなど,ADの総合的な検証フレームワークを提案する。 最も重要なことは、モデルをベースとした手法を用いて、完全自動検証のための変換アルゴリズムを開発し、QASCADと呼ばれるツールで実装したことです。
  論文  参考訳（メタデータ） (2024-02-29T22:40:39Z)
• Lemur: Integrating Large Language Models in Automated Program Verification [10.221822902660458]
  自動プログラム検証のためのLLMと自動推論器のパワーを組み合わせるための一般的な手法を提案する。 本稿では,音声自動検証手法として計算をインスタンス化し,一連の合成および競合ベンチマークの実践的改善を実証する。
  論文  参考訳（メタデータ） (2023-10-07T16:44:53Z)
• A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis [54.959571890098786]
  システム仕様を符号化し、対応する証明書を定義するためのフレームワークを提供する。 コントローラと証明書を形式的に合成する自動化手法を提案する。 我々のアプローチは、ニューラルネットワークの柔軟性を利用して、制御のための安全な学習の幅広い分野に寄与する。
  論文  参考訳（メタデータ） (2023-09-12T09:37:26Z)
• On the Limits of Evaluating Embodied Agent Model Generalization Using Validation Sets [101.28658250723804]
  本稿では,より広い視野を効果的に活用し,次のステップでナビゲーションや操作を行うかを選択するモジュールによるトランスフォーマーモデルの拡張実験を行う。 提案したモジュールは改良され,実際に,一般的なベンチマークデータセットであるALFREDの未確認検証セット上での最先端のパフォーマンスが向上した。 この結果は、機械学習タスクではより広い現象かもしれないが、主にテストスプリットの評価を制限するベンチマークでのみ顕著である、と我々は考えているので強調する。
  論文  参考訳（メタデータ） (2022-05-18T23:52:21Z)
• Automated Aggregator -- Rewriting with the Counting Aggregate [0.0]
  本稿では,補完的な性能を持つ等価プログラム群を生成する自動書き換えシステムを提案する。 本稿では,自動解答器選択ツールにおけるシステムの利用を提案する。
  論文  参考訳（メタデータ） (2020-09-22T00:48:33Z)
• Generating Fact Checking Explanations [52.879658637466605]
  まだ欠けているパズルの重要なピースは、プロセスの最も精巧な部分を自動化する方法を理解することです。 本稿では、これらの説明を利用可能なクレームコンテキストに基づいて自動生成する方法について、最初の研究を行う。 この結果から,個別に学習するのではなく,両目標を同時に最適化することで,事実確認システムの性能が向上することが示唆された。
  論文  参考訳（メタデータ） (2020-04-13T05:23:25Z)

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

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