論文の概要: AutoDeduct: A Tool for Automated Deductive Verification of C Code

• arxiv url: http://arxiv.org/abs/2501.10889v1
• Date: Sat, 18 Jan 2025 22:00:43 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-01-22 14:23:34.255864
• Title: AutoDeduct: A Tool for Automated Deductive Verification of C Code
• Title（参考訳）: AutoDeduct: Cコードのデダクティブ検証を自動化するツール
• Authors: Jesper Amilon, Dilian Gurov, Christian Lidström, Mattias Nyberg, Gustav Ung, Ola Wingbrant,
• Abstract要約: 私たちはFrama-Cフレームワーク上に構築されたAutoDeductツールチェーンを紹介します。 Cプログラムの関数のコントラクトを自動的に推論するテクニックの組み合わせを実装している。 AutoDeductの現在のリリースは、最初のパブリックプロトタイプである。
• 参考スコア（独自算出の注目度）: 0.3518504468878697
• License:
• Abstract: Deductive verification has become a mature paradigm for the verification of industrial software. Applying deductive verification, however, requires that every function in the code base is annotated with a function contract specifying its behaviour. This introduces a large overhead of manual work. To address this challenge, we introduce the AutoDeduct toolchain, built on top of the Frama-C framework. It implements a combination of techniques to automatically infer contracts for functions in C programs, in the syntax of ACSL, the specification language of Frama-C. Contract inference in AutoDecuct is implemented as two plugins for Frama-C, each inferring different types of annotations. We assume that programs have an entry-point function already equipped with a contract, which is used in conjunction with the program source code to infer contracts for the helper functions, so that the entry-point contract can be verified. The current release of AutoDeduct is the first public prototype, which we evaluate on an example adapted from industrial software.
• Abstract（参考訳）: 導出検証は、産業用ソフトウェアの検証において成熟したパラダイムとなっている。 しかし、帰納的検証を適用するには、コードベースのすべての関数に、その振る舞いを指定する関数コントラクトをアノテートする必要がある。 これは手作業の大きなオーバーヘッドをもたらす。 この課題に対処するために、Frama-Cフレームワーク上に構築されたAutoDeductツールチェーンを紹介します。 これは、Frama-Cの仕様言語であるACSLの構文において、Cプログラムの関数のコントラクトを自動的に推論する技術の組み合わせを実装している。 AutoDecuctのコントラクト推論はFrama-C用の2つのプラグインとして実装されている。 本稿では,プログラムのソースコードと連動して,ヘルパー関数の契約を推論し,エントリポイントの契約を検証できるように,すでにあるエントリポイント関数がプログラムのソースコードに組み込まれていると仮定する。 AutoDeductの現在のリリースは、最初のパブリックプロトタイプであり、産業用ソフトウェアから適応した例に基づいて評価する。

関連論文リスト

• Correctness Witnesses with Function Contracts [0.1499944454332829]
  我々は、関数契約の仕様化を可能にするために、既存の証人フォーマット2.0の拡張を提案する。 これにより、ツールからより多くの情報をエクスポートしたり、機能コントラクトを必要とするツールと情報を交換することが可能になる。
  論文  参考訳（メタデータ） (2025-01-21T17:27:59Z)
• COBRA: Interaction-Aware Bytecode-Level Vulnerability Detector for Smart Contracts [4.891180928768215]
  スマートコントラクトの脆弱性を検出するために,セマンティックコンテキストと関数インターフェースを統合したフレームワークであるCOBRAを提案する。 署名データベースに存在しない関数シグネチャを推測するために,スマートコントラクトバイトコードから関数シグネチャの規則を自動的に学習するSRIFを提案する。 実験の結果、SRIFは関数シグネチャ推論において94.76%のF1スコアを達成できることが示された。
  論文  参考訳（メタデータ） (2024-10-28T03:55:09Z)
• SEP: Self-Enhanced Prompt Tuning for Visual-Language Model [93.94454894142413]
  SEP(Self-Enhanced Prompt Tuning)という新しいアプローチを導入する。 SEPは、テキストレベルの埋め込みと視覚レベルの埋め込みの両方を強化するために、差別的な事前知識を明示的に取り入れている。 様々なベンチマークやタスクの総合的な評価は、プロンプトチューニングにおけるSEPの有効性を確認している。
  論文  参考訳（メタデータ） (2024-05-24T13:35:56Z)
• CELA: Cost-Efficient Language Model Alignment for CTR Prediction [70.65910069412944]
  CTR(Click-Through Rate)予測は、レコメンダシステムにおいて最重要位置を占める。 最近の取り組みは、プレトレーニング言語モデル(PLM)を統合することでこれらの課題を緩和しようとしている。 CTR予測のためのtextbfCost-textbfEfficient textbfLanguage Model textbfAlignment (textbfCELA)を提案する。
  論文  参考訳（メタデータ） (2024-05-17T07:43:25Z)
• General Point Model with Autoencoding and Autoregressive [55.051626723729896]
  本稿では,ポイントクラウドトランスにおける自動エンコーディングと自己回帰タスクをシームレスに統合する汎用ポイントモデルを提案する。 このモデルは汎用性が高く、ダウンストリームポイントクラウド表現タスクの微調整や、条件なしおよび条件付き生成タスクが可能である。
  論文  参考訳（メタデータ） (2023-10-25T06:08:24Z)
• Generalizable Chain-of-Thought Prompting in Mixed-task Scenarios with Large Language Models [68.05046964022844]
  大規模言語モデル(LLM)は、チェーン・オブ・ソート(CoT)のプロンプトを活用することで、顕著な推論機能を明らかにしている。 本稿では,入力質問の種類が不明な混合タスクシナリオにおいて,一般化可能なCoTプロンプト機構であるGeM-CoTを提案する。 この技術設計により、GeM-CoTは10の公開推論タスクと23のBBHタスクにおいて優れた一般化能力と優れたパフォーマンスを同時に享受する。
  論文  参考訳（メタデータ） (2023-10-10T15:10:03Z)
• Automatic Program Instrumentation for Automatic Verification (Extended Technical Report) [0.0]
  帰納的検証とソフトウェアモデルチェックでは、特定の仕様言語構造を扱うことが問題となる。 本稿では,様々なアドホックなアプローチを仮定する統一検証パラダイムとして,インスツルメンテーションを提案する。 我々は,プログラムのアグリゲーションによる検証に適したMonoCeraツールにアプローチを実装した。
  論文  参考訳（メタデータ） (2023-05-26T14:55:35Z)
• Verified Reversible Programming for Verified Lossless Compression [11.020543186794459]
  ロスレス圧縮の実装は通常、エンコーダとデコーダの2つのプログラムを含む。 我々は、非対称数値システム(ANS)に基づく圧縮手法のかなりのクラスが、エンコーダとデコーダの間で共有構造を持つことを観察する。 私たちはAgdaに埋め込まれた小さな可逆言語「Flipper」を実装しました。
  論文  参考訳（メタデータ） (2022-11-02T16:39:41Z)
• Binding Language Models in Symbolic Languages [146.3027328556881]
  Binderはトレーニング不要のニューラルシンボリックフレームワークで、タスク入力をプログラムにマッピングする。 解析の段階では、Codexは元のプログラミング言語では答えられないタスク入力の一部を特定することができる。 実行段階では、CodexはAPI呼び出しで適切なプロンプトを与えられた万能機能を実行することができる。
  論文  参考訳（メタデータ） (2022-10-06T12:55:17Z)
• CodeT5: Identifier-aware Unified Pre-trained Encoder-Decoder Models for Code Understanding and Generation [36.47905744758698]
  我々は、開発者が指定した識別子から伝達されるコードセマンティクスをよりよく活用する、事前訓練されたエンコーダ-デコーダ変換モデルであるCodeT5を提案する。 我々のモデルは、コード理解と生成タスクの両方をシームレスにサポートし、マルチタスク学習を可能にする統一的なフレームワークを採用している。
  論文  参考訳（メタデータ） (2021-09-02T12:21:06Z)
• Autoencoding Variational Autoencoder [56.05008520271406]
  我々は,この行動が学習表現に与える影響と,自己整合性の概念を導入することでそれを修正する結果について検討する。 自己整合性アプローチで訓練されたエンコーダは、敵攻撃による入力の摂動に対して頑健な(無神経な)表現につながることを示す。
  論文  参考訳（メタデータ） (2020-12-07T14:16:14Z)

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

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