論文の概要: Correctness Witnesses with Function Contracts

• arxiv url: http://arxiv.org/abs/2501.12313v1
• Date: Tue, 21 Jan 2025 17:27:59 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-01-22 14:23:29.061183
• Title: Correctness Witnesses with Function Contracts
• Title（参考訳）: 関数契約による正当性ウィットネス
• Authors: Matthias Heizmann, Dominik Klumpp, Marian Lingsch-Rosenfeld, Frank Schüssele,
• Abstract要約: 我々は、関数契約の仕様化を可能にするために、既存の証人フォーマット2.0の拡張を提案する。 これにより、ツールからより多くの情報をエクスポートしたり、機能コントラクトを必要とするツールと情報を交換することが可能になる。
• 参考スコア（独自算出の注目度）: 0.1499944454332829
• License:
• Abstract: Software verification witnesses are a common exchange format for software verification tools. They were developed to provide arguments supporting the verification result, allowing other tools to reproduce the verification results. Correctness witnesses in the current format (version 2.0) allow only for the encoding of loop and location invariants using C expressions. This limits the correctness arguments that verifiers can express in the witness format. One particular limitation is the inability to express function contracts, which consist of a pre-condition and a post-condition for a function. We propose an extension to the existing witness format 2.0 to allow for the specification of function contracts. Our extension includes support for several features inspired by ACSL (\result, \old, \at). This allows for the export of more information from tools and for the exchange of information with tools that require function contracts.
• Abstract（参考訳）: ソフトウェア検証証人は、ソフトウェア検証ツールの共通の交換フォーマットである。 それらは検証結果を支持する議論を提供するために開発され、他のツールで検証結果の再現を可能にした。 現在のフォーマット(バージョン2.0)の正確さの証人は、C式を使ってループと位置不変量のエンコーディングしかできない。 これにより、検証者が証人形式で表現できる正当性引数が制限される。 1つの制限は、関数の事前条件と後条件からなる関数コントラクトを表現できないことである。 我々は、関数契約の仕様化を可能にするために、既存の証人フォーマット2.0の拡張を提案する。 私たちの拡張には、ACSL(\result, \old, \at)にインスパイアされたいくつかの機能のサポートが含まれています。 これにより、ツールからより多くの情報をエクスポートしたり、機能コントラクトを必要とするツールと情報を交換することが可能になる。

関連論文リスト

• COBRA: Interaction-Aware Bytecode-Level Vulnerability Detector for Smart Contracts [4.891180928768215]
  スマートコントラクトの脆弱性を検出するために,セマンティックコンテキストと関数インターフェースを統合したフレームワークであるCOBRAを提案する。 署名データベースに存在しない関数シグネチャを推測するために,スマートコントラクトバイトコードから関数シグネチャの規則を自動的に学習するSRIFを提案する。 実験の結果、SRIFは関数シグネチャ推論において94.76%のF1スコアを達成できることが示された。
  論文  参考訳（メタデータ） (2024-10-28T03:55:09Z)
• Enhancing Translation Validation of Compiler Transformations with Large Language Models [5.103162976634333]
  本稿では,Large Language Models (LLM) を翻訳検証に組み込むフレームワークを提案する。 まず,既存の形式検証ツールを用いて翻訳検証を行う。 フォーマルな検証ツールが変換の健全性を確認することができない場合、我々のフレームワークは予測に微調整のLLMを用いる。
  論文  参考訳（メタデータ） (2024-01-30T07:24:04Z)
• An Efficient VCGen-based Modular Verification of Relational Properties [1.567576360103422]
  帰納的検証は通常、単一の関数呼び出しに対して各関数の振舞いを指定する関数コントラクトに依存します。 近年の研究では,検証条件生成に依存する関係性検証手法が提案されている。
  論文  参考訳（メタデータ） (2024-01-16T14:19:04Z)
• Factcheck-Bench: Fine-Grained Evaluation Benchmark for Automatic Fact-checkers [121.53749383203792]
  本稿では,大規模言語モデル (LLM) 生成応答の事実性に注釈を付けるための総合的なエンドツーエンドソリューションを提案する。 オープンドメインの文書レベルの事実性ベンチマークを,クレーム,文,文書の3段階の粒度で構築する。 予備実験によると、FacTool、FactScore、Perplexityは虚偽の主張を識別するのに苦労している。
  論文  参考訳（メタデータ） (2023-11-15T14:41:57Z)
• Knowledge-Augmented Language Model Verification [68.6099592486075]
  最近の言語モデル(LM)は、パラメータに内在化された知識を持つテキストを生成する際、印象的な能力を示している。 本稿では,知識付加型LMの出力と知識を別個の検証器で検証することを提案する。 その結果,提案した検証器は,検索と生成の誤りを効果的に識別し,LMがより現実的に正しい出力を提供できることを示した。
  論文  参考訳（メタデータ） (2023-10-19T15:40:00Z)
• Towards Formal Verification of a TPM Software Stack [0.5074812070492739]
  本稿では,Frama-C 検証プラットフォームを用いた tpm2-ts の形式的検証について述べる。 リンクされたリストと複雑なデータ構造に基づいて、ライブラリのコードは検証ツールにとって非常に難しいように思える。
  論文  参考訳（メタデータ） (2023-07-31T16:35:16Z)
• FacTool: Factuality Detection in Generative AI -- A Tool Augmented Framework for Multi-Task and Multi-Domain Scenarios [87.12753459582116]
  より広い範囲のタスクは、生成モデルによって処理されると、事実エラーを含むリスクが増大する。 大規模言語モデルにより生成されたテキストの事実誤りを検出するためのタスクおよびドメインに依存しないフレームワークであるFacToolを提案する。
  論文  参考訳（メタデータ） (2023-07-25T14:20:51Z)
• Give Me More Details: Improving Fact-Checking with Latent Retrieval [58.706972228039604]
  証拠は、自動化された事実チェックにおいて重要な役割を果たす。 既存のファクトチェックシステムは、エビデンス文が与えられたと仮定するか、検索エンジンが返した検索スニペットを使用する。 資料から得られた全文を証拠として組み込んで,2つの豊富なデータセットを導入することを提案する。
  論文  参考訳（メタデータ） (2023-05-25T15:01:19Z)
• Auditing AI models for Verified Deployment under Semantic Specifications [65.12401653917838]
  AuditAIは、解釈可能な形式検証とスケーラビリティのギャップを埋める。 AuditAIは、画素空間の摂動のみを用いた検証の限界に対処しながら、検証と認定トレーニングのための制御されたバリエーションを得られるかを示す。
  論文  参考訳（メタデータ） (2021-09-25T22:53:24Z)

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

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