論文の概要: 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プログラムを含むサンプルプログラムで評価する。
関連論文リスト
- Quantitative Assurance and Synthesis of Controllers from Activity
Diagrams [4.419843514606336]
確率的モデル検査は、定性的および定量的な性質を自動検証するために広く用いられている形式的検証手法である。
これにより、必要な知識を持っていない研究者やエンジニアにはアクセスできない。
本稿では,確率時間の新しいプロファイル,品質アノテーション,3つのマルコフモデルにおけるADの意味論的解釈,アクティビティ図からPRISM言語への変換ルールのセットなど,ADの総合的な検証フレームワークを提案する。
最も重要なことは、モデルをベースとした手法を用いて、完全自動検証のための変換アルゴリズムを開発し、QASCADと呼ばれるツールで実装したことです。
論文 参考訳(メタデータ) (2024-02-29T22:40:39Z) - Counting Reward Automata: Sample Efficient Reinforcement Learning
Through the Exploitation of Reward Function Structure [13.231546105751015]
本稿では,形式言語として表現可能な任意の報酬関数をモデル化可能な有限状態機械変種であるカウント・リワード・オートマトンを提案する。
このような抽象機械を組み込んだエージェントが,現在の手法よりも大きなタスクの集合を解くことができることを実証する。
論文 参考訳(メタデータ) (2023-12-18T17:20:38Z) - Lemur: Integrating Large Language Models in Automated Program
Verification [11.488304563932866]
自動プログラム検証のためのLLMと自動推論器のパワーを組み合わせるための一般的な手法を提案する。
計算を音響自動検証の手順としてインスタンス化し、一連の合成および競合ベンチマークを実践的に改善した。
論文 参考訳(メタデータ) (2023-10-07T16:44:53Z) - A General Verification Framework for Dynamical and Control Models via
Certificate Synthesis [60.03938402120854]
システム仕様を符号化し、対応する証明書を定義するためのフレームワークを提供する。
コントローラと証明書を形式的に合成する自動化手法を提案する。
我々のアプローチは、ニューラルネットワークの柔軟性を利用して、制御のための安全な学習の幅広い分野に寄与する。
論文 参考訳(メタデータ) (2023-09-12T09:37:26Z) - Generating Sequences by Learning to Self-Correct [64.0249217590888]
自己補正(Self-Correction)は、不完全な世代を反復的に修正する独立した修正器から不完全なベースジェネレータを分離する。
本稿では,3つの多種多様なタスクにおいて,自己補正がベースジェネレータを改善することを示す。
論文 参考訳(メタデータ) (2022-10-31T18:09:51Z) - Relational Action Bases: Formalization, Effective Safety Verification,
and Invariants (Extended Version) [67.99023219822564]
我々はリレーショナルアクションベース(RAB)の一般的な枠組みを紹介する。
RABは両方の制限を解除することで既存のモデルを一般化する。
データ対応ビジネスプロセスのベンチマークにおいて、このアプローチの有効性を実証する。
論文 参考訳(メタデータ) (2022-08-12T17:03:50Z) - On the Limits of Evaluating Embodied Agent Model Generalization Using
Validation Sets [101.28658250723804]
本稿では,より広い視野を効果的に活用し,次のステップでナビゲーションや操作を行うかを選択するモジュールによるトランスフォーマーモデルの拡張実験を行う。
提案したモジュールは改良され,実際に,一般的なベンチマークデータセットであるALFREDの未確認検証セット上での最先端のパフォーマンスが向上した。
この結果は、機械学習タスクではより広い現象かもしれないが、主にテストスプリットの評価を制限するベンチマークでのみ顕著である、と我々は考えているので強調する。
論文 参考訳(メタデータ) (2022-05-18T23:52:21Z) - Parallel and Multi-Objective Falsification with Scenic and VerifAI [11.152087017964584]
シナリオ仕様言語とVerifAIツールキットの拡張について述べる。
まず,Scanicのシミュレーションとサンプリング機能の両方にインタフェースを組み込んだ並列化フレームワークを提案する。
次に、サンプリング中の多目的最適化をサポートするために、VerifAIのファルシフィケーションアルゴリズムの拡張を示す。
論文 参考訳(メタデータ) (2021-07-09T01:08:49Z) - CoCoMoT: Conformance Checking of Multi-Perspective Processes via SMT
(Extended Version) [62.96267257163426]
我々はCoCoMoT(Computing Conformance Modulo Theories)フレームワークを紹介する。
まず、純粋な制御フロー設定で研究したSATベースのエンコーディングを、データ認識ケースに持ち上げる方法を示す。
次に,プロパティ保存型クラスタリングの概念に基づく新しい前処理手法を提案する。
論文 参考訳(メタデータ) (2021-03-18T20:22:50Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。