論文の概要: Execution Time Program Verification With Tight Bounds
- arxiv url: http://arxiv.org/abs/2210.11105v1
- Date: Thu, 20 Oct 2022 09:02:13 GMT
- ステータス: 処理完了
- システム内更新日: 2022-10-21 14:33:29.088516
- Title: Execution Time Program Verification With Tight Bounds
- Title（参考訳）: タイト境界による実行時間プログラム検証
- Authors: Ana Carolina Silva, Manuel Barbosa and Mario Florido
- Abstract要約: 本稿では,コア命令型プログラミング言語の実行時間境界を推論するための証明システムを提案する。
3つのケースに対してHoareロジックを定義し、注釈付きコスト対応操作セマンティクスに関してその健全性を証明する。
証明システムの実用性は、サンプルプログラムに適用するために必要な異なるモジュールのOCamlの実装で実証される。
- 参考スコア（独自算出の注目度）: 6.36836017515443
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: This paper presents a proof system for reasoning about execution time bounds
for a core imperative programming language. Proof systems are defined for three
different scenarios: approximations of the worst-case execution time, exact
time reasoning, and less pessimistic execution time estimation using amortized
analysis. We define a Hoare logic for the three cases and prove its soundness
with respect to an annotated cost-aware operational semantics. Finally, we
define a verification conditions (VC) generator that generates the goals needed
to prove program correctness, cost, and termination. Those goals are then sent
to the Easycrypt toolset for validation. The practicality of the proof system
is demonstrated with an implementation in OCaml of the different modules needed
to apply it to example programs. Our case studies are motivated by real-time
and cryptographic software.
- Abstract（参考訳）: 本稿では,コア命令型プログラミング言語の実行時間境界を推論するための証明システムを提案する。
証明システムは3つの異なるシナリオで定義されている: 最悪の場合の実行時間の近似、正確な時間推論、償却分析による悲観的実行時間の推定。
3つのケースに対してHoareロジックを定義し、注釈付きコスト対応操作意味論に関してその健全性を証明する。
最後に、プログラムの正確性、コスト、終了の証明に必要なゴールを生成する検証条件(VC)の生成を定義する。
それらの目標は、検証のためにeasycryptツールセットに送られる。
証明システムの実用性は,ocamlで実装したサンプルプログラムに適用するために必要なモジュールによって実証される。
私たちのケーススタディは、リアルタイムおよび暗号化ソフトウェアが動機です。
関連論文リスト
- FIRE: Fact-checking with Iterative Retrieval and Verification [63.67320352038525]
FIREはエビデンス検索とクレーム検証を反復的に統合する新しいフレームワークである。
大きな言語モデル(LLM)のコストを平均7.6倍、検索コストを16.5倍削減しながら、パフォーマンスが若干向上している。
これらの結果から,FIREは大規模ファクトチェック業務における適用を約束していることが明らかとなった。
論文 参考訳（メタデータ） (2024-10-17T06:44:18Z) - Inductive Predicate Synthesis Modulo Programs (Extended) [1.7372615815088566]
プログラム解析のトレンドは、入力プログラムの言語内で検証条件を符号化することである。
Inductive Predicate Synthesis Modulo Programs (IPS-MP) を提案する。
論文 参考訳（メタデータ） (2024-07-11T12:51:08Z) - Evaluating LLM-driven User-Intent Formalization for Verification-Aware Languages [6.0608817611709735]
本稿では,検証対応言語における仕様の質を評価するための指標を提案する。
MBPPコード生成ベンチマークのDafny仕様の人間ラベル付きデータセットに,我々の測定値が密接に一致することを示す。
また、このテクニックをより広く適用するために対処する必要がある正式な検証課題についても概説する。
論文 参考訳（メタデータ） (2024-06-14T06:52:08Z) - Bisimulation Learning [55.859538562698496]
我々は、大きな、潜在的に無限の状態空間を持つ状態遷移系の有限バイシミュレートを計算する。
提案手法は,実際に行われている他の最先端ツールよりも高速な検証結果が得られる。
論文 参考訳（メタデータ） (2024-05-24T17:11:27Z) - NExT: Teaching Large Language Models to Reason about Code Execution [50.93581376646064]
大規模言語モデル(LLM)のコードは通常、プログラムの表面テキスト形式に基づいて訓練される。
NExTは,プログラムの実行トレースを検査し,実行時の動作を判断する手法である。
論文 参考訳（メタデータ） (2024-04-23T01:46:32Z) - Parallel Program Analysis on Path Ranges [3.018638214344819]
Ranged symbolic execution は、並列にパス範囲と呼ばれるプログラム部分でシンボリックな実行を実行する。
本稿では,プログラムを経路範囲に分割し,任意の解析を並列に行う検証手法を提案する。
論文 参考訳（メタデータ） (2024-02-19T08:26:52Z) - Decidable Reasoning About Time in Finite-Domain Situation Calculus
Theories [9.45355418401911]
最も一般的に使用されるアプローチは、実値の流れる$mathittime(a)$を追加して、各アクションにタイムポイントをアタッチし、結果として各状況にアタッチすることで、時間を表す。
このアプローチでは、言論の領域が有限個の対象に制限されている場合でも、与えられた式を満たす到達可能な状況が決定不能であるかどうかを確認する。
論文 参考訳（メタデータ） (2024-02-05T16:32:12Z) - Unlocking Temporal Question Answering for Large Language Models with Tailor-Made Reasoning Logic [84.59255070520673]
大きな言語モデル(LLM)は、時間的推論に関わる際に課題に直面します。
本研究では,時間的質問応答タスクに特化して設計された新しいフレームワークであるTempLogicを提案する。
論文 参考訳（メタデータ） (2023-05-24T10:57:53Z) - Fact-Checking Complex Claims with Program-Guided Reasoning [99.7212240712869]
Program-Guided Fact-Checking (ProgramFC)は、複雑なクレームを単純なサブタスクに分解する新しいファクトチェックモデルである。
まず,大規模言語モデルの文脈内学習能力を活用して推論プログラムを生成する。
我々は,各サブタスクを対応するサブタスクハンドラに委譲することでプログラムを実行する。
論文 参考訳（メタデータ） (2023-05-22T06:11:15Z) - Time-varying Gaussian Process Bandit Optimization with Non-constant
Evaluation Time [93.6788993843846]
非定常評価時間を効果的に処理できる新しい時間変化ベイズ最適化アルゴリズムを提案する。
我々の限界は、評価時間列のパターンが問題の難易度に大きな影響を与えることを決定づける。
論文 参考訳（メタデータ） (2020-03-10T13:28:33Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。