論文の概要: 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で実装したサンプルプログラムに適用するために必要なモジュールによって実証される。
私たちのケーススタディは、リアルタイムおよび暗号化ソフトウェアが動機です。
関連論文リスト
- Parallel Program Analysis on Path Ranges [3.2976453916809803]
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) - Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic [4.60607942851373]
システム実行から形式仕様を自動合成する問題を考察する。
時間論理式を合成するための古典的なアプローチの多くは、公式のサイズを最小化することを目的としている。
我々は,この概念を定式化し,有界な外見を持つ簡潔な公式を合成する学習アルゴリズムを考案する。
論文 参考訳(メタデータ) (2023-10-26T14:13:15Z) - SAT-based Formal Fault-Resistance Verification of Cryptographic Circuits [4.42563968195381]
本稿では,NP完全であることを示す耐故障性検証問題を定式化する。
そこで我々は,耐故障性検証問題をBoolean satisfiability (SAT)問題として符号化する新しい手法を考案した。
この手法は、リアルな暗号回路ベンチマークで広く評価されているオープンソースツールFIRMERで実装されている。
論文 参考訳(メタデータ) (2023-07-02T13:01:32Z) - Code Prompting: a Neural Symbolic Method for Complex Reasoning in Large
Language Models [74.95486528482327]
コードプロンプト(code prompting)は、ゼロショットバージョンと少数ショットバージョンの両方を持ち、中間ステップとしてコードをトリガーするニューラルシンボルプロンプトである。
我々は,記号的推論と算術的推論を含む7つの広く使用されているベンチマーク実験を行った。
論文 参考訳(メタデータ) (2023-05-29T15:14:09Z) - Fact-Checking Complex Claims with Program-Guided Reasoning [99.7212240712869]
Program-Guided Fact-Checking (ProgramFC)は、複雑なクレームを単純なサブタスクに分解する新しいファクトチェックモデルである。
まず,大規模言語モデルの文脈内学習能力を活用して推論プログラムを生成する。
我々は,各サブタスクを対応するサブタスクハンドラに委譲することでプログラムを実行する。
論文 参考訳(メタデータ) (2023-05-22T06:11:15Z) - Fault-Aware Neural Code Rankers [64.41888054066861]
サンプルプログラムの正しさを予測できる故障認識型ニューラルネットワークローダを提案する。
我々のフォールト・アウェア・ローダは、様々なコード生成モデルのpass@1精度を大幅に向上させることができる。
論文 参考訳(メタデータ) (2022-06-04T22:01:05Z) - From Checking to Inference: Actual Causality Computations as
Optimization Problems [79.87179017975235]
本稿では、最適化問題として二元非巡回モデルよりも、因果推論の異なる概念を定式化するための新しいアプローチを提案する。
8000ドル以上の変数を持つモデルを用いて,MaxSAT が ILP を上回り,数秒単位でチェック処理を行う場合が多い。
論文 参考訳(メタデータ) (2020-06-05T10:56:52Z) - Self-Supervised Log Parsing [59.04636530383049]
大規模ソフトウェアシステムは、大量の半構造化ログレコードを生成する。
既存のアプローチは、ログ特化や手動ルール抽出に依存している。
本稿では,自己教師付き学習モデルを用いて解析タスクをマスク言語モデリングとして定式化するNuLogを提案する。
論文 参考訳(メタデータ) (2020-03-17T19:25:25Z) - Construe: a software solution for the explanation-based interpretation
of time series [0.0]
本稿では,帰納的推論に基づく時系列解釈のための汎用フレームワークのソフトウェア実装について述べる。
概念実証として、心電図(ECG)領域の総合的な知識ベースが提供され、心電図解析のツールとして直接使用できる。
論文 参考訳(メタデータ) (2020-03-17T09:26:55Z) - Time-varying Gaussian Process Bandit Optimization with Non-constant
Evaluation Time [93.6788993843846]
非定常評価時間を効果的に処理できる新しい時間変化ベイズ最適化アルゴリズムを提案する。
我々の限界は、評価時間列のパターンが問題の難易度に大きな影響を与えることを決定づける。
論文 参考訳(メタデータ) (2020-03-10T13:28:33Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。