論文の概要: A Unit Proofing Framework for Code-level Verification: A Research Agenda

• arxiv url: http://arxiv.org/abs/2410.14818v2
• Date: Wed, 30 Apr 2025 14:34:05 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-05-02 19:15:52.100314
• Title: A Unit Proofing Framework for Code-level Verification: A Research Agenda
• Title（参考訳）: コードレベルの検証のためのユニットプロファイリングフレームワーク:リサーチアジェンダ
• Authors: Paschal C. Amusuo, Parth V. Patil, Owen Cochell, Taylor Le Lievre, James C. Davis,
• Abstract要約: 本稿では,方法論とツールの両面から,単体証明フレームワークの研究課題を提案する。 これにより、エンジニアはコードレベルの欠陥を早期に発見できる。
• 参考スコア（独自算出の注目度）: 2.7325338323814328
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: Formal verification provides mathematical guarantees that a software is correct. Design-level verification tools ensure software specifications are correct, but they do not expose defects in actual implementations. For this purpose, engineers use code-level tools. However, such tools struggle to scale to large software. The process of "Unit Proofing" mitigates this by decomposing the software and verifying each unit independently. We examined AWS's use of unit proofing and observed that current approaches are manual and prone to faults that mask severe defects. We propose a research agenda for a unit proofing framework, both methods and tools, to support software engineers in applying unit proofing effectively and efficiently. This will enable engineers to discover code-level defects early.
• Abstract（参考訳）: 形式検証は、ソフトウェアが正しいという数学的保証を提供する。 設計レベルの検証ツールは、ソフトウェア仕様が正しいことを保証するが、実際の実装の欠陥は明らかにしない。 この目的のために、エンジニアはコードレベルのツールを使用する。 しかし、そのようなツールは大規模なソフトウェアにスケールするのに苦労する。 のプロセスは、ソフトウェアを分解し、各ユニットを独立して検証することでこれを緩和します。 私たちは、AWSのユニット検証の使用を調査し、現在のアプローチが手作業であり、深刻な欠陥を隠蔽する欠陥があることを示した。 本稿では,ソフトウェア技術者が効果的かつ効率的にユニット検証を行うことを支援するための,手法とツールの両面から,ユニット検証フレームワークの研究課題を提案する。 これにより、エンジニアはコードレベルの欠陥を早期に発見できる。

関連論文リスト

• Do Unit Proofs Work? An Empirical Study of Compositional Bounded Model Checking for Memory Safety Verification [4.826167697662746]
  メモリ安全性の欠陥は、ソフトウェアの信頼性に大きな脅威をもたらし、サイバー攻撃、停電、クラッシュを可能にします。 これらのリスクを軽減するため、組織はコンポジション境界モデルチェック(BMC)を採用し、ユニット証明を使用してメモリ安全性を正式に検証する。 しかし、ユニットテストを作成する方法は組織によって異なり、同じプロジェクト内で一貫性がないため、エラーや欠陥が失われる。 本研究は,メモリ安全性検証のためのユニット証明に関する最初の実証的研究である。
  論文  参考訳（メタデータ） (2025-03-17T22:55:12Z)
• ToolFuzz -- Automated Agent Tool Testing [5.174808367448261]
  ToolFuzzは,(1)ツール実行時のエラーにつながるユーザクエリと,(2)誤ったエージェント応答につながるユーザクエリの2つのタイプのエラーを検出するように設計されている。 ToolFuzzは、プロンプトエンジニアリングのアプローチと比較して、20倍の誤入力を識別する。
  論文  参考訳（メタデータ） (2025-03-06T14:29:52Z)
• ToolCoder: A Systematic Code-Empowered Tool Learning Framework for Large Language Models [49.04652315815501]
  ツール学習は、大規模な言語モデル(LLM)にとって、外部ツールとのインタラクションを通じて、複雑な現実世界のタスクを解決する重要な機能として登場した。 本稿では,ツール学習をコード生成タスクとして再編成する新しいフレームワークであるToolCoderを提案する。
  論文  参考訳（メタデータ） (2025-02-17T03:42:28Z)
• Verifying Non-friendly Formal Verification Designs: Can We Start Earlier? [2.1626093085892144]
  本稿では,2つの主要なステップからなるメタモデリング技術に基づく自動手法を提案する。 まず、C++で書かれた未使用のアルゴリズム記述を、生成されたアサーションを使用して早期に検証する。 第2に、HLECとそのメタモデルパラメータを用いて、このアルゴリズム記述をシーケンシャルな設計に対して検証する。
  論文  参考訳（メタデータ） (2024-10-24T06:09:40Z)
• Learning to Ask: When LLM Agents Meet Unclear Instruction [55.65312637965779]
  大きな言語モデル(LLM)は、言語スキルだけでは達成不可能なタスクに対処するための外部ツールを活用することができる。 我々は、不完全な命令下でのLLMツールの使用性能を評価し、エラーパターンを分析し、Noisy ToolBenchと呼ばれる挑戦的なツール使用ベンチマークを構築した。 Ask-when-Needed (AwN) という新しいフレームワークを提案する。
  論文  参考訳（メタデータ） (2024-08-31T23:06:12Z)
• NExT: Teaching Large Language Models to Reason about Code Execution [50.93581376646064]
  大規模言語モデル(LLM)のコードは通常、プログラムの表面テキスト形式に基づいて訓練される。 NExTは,プログラムの実行トレースを検査し,実行時の動作を判断する手法である。
  論文  参考訳（メタデータ） (2024-04-23T01:46:32Z)
• GenAudit: Fixing Factual Errors in Language Model Outputs with Evidence [64.95492752484171]
  GenAudit - 文書基底タスクの事実チェック LLM 応答を支援するためのツール。 これらのタスクを実行するためにモデルをトレーニングし、ユーザに対して推奨の編集とエビデンスを示すインタラクティブインターフェースを設計します。 システムによってほとんどのエラーがフラグ付けされていることを保証するため,精度への影響を最小限に抑えつつエラーリコールを増大させる手法を提案する。
  論文  参考訳（メタデータ） (2024-02-19T21:45:55Z)
• Klever: Verification Framework for Critical Industrial C Programs [0.0]
  我々は,大規模かつ重要な産業用Cプログラムに自動ソフトウェア検証ツールを適用する労力を削減するために,Kleverソフトウェア検証フレームワークを提案する。 既存のツールは、環境モデリング、要件の仕様、ターゲットプログラムの多くのバージョンと構成の検証、検証結果のエキスパートアセスメントなど、広く採用されている手段を提供していない。
  論文  参考訳（メタデータ） (2023-09-28T13:23:59Z)
• 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)
• Applying Machine Learning Analysis for Software Quality Test [0.0]
  メンテナンスのトリガーと予測されるかどうかを理解することは重要です。 生成したプログラムの複雑さを評価する多くの手法は有用な予測モデルを生成する。 本稿では,機械学習を利用可能なデータに適用し,累積ソフトウェア故障レベルを算出する。
  論文  参考訳（メタデータ） (2023-05-16T06:10:54Z)
• Generation Probabilities Are Not Enough: Uncertainty Highlighting in AI Code Completions [54.55334589363247]
  本研究では,不確実性に関する情報を伝達することで,プログラマがより迅速かつ正確にコードを生成することができるかどうかを検討する。 トークンのハイライトは、編集される可能性が最も高いので、タスクの完了が早くなり、よりターゲットを絞った編集が可能になることがわかりました。
  論文  参考訳（メタデータ） (2023-02-14T18:43:34Z)
• Lessons from Formally Verified Deployed Software Systems (Extended version) [65.69802414600832]
  本稿は、正式に認証されたシステムを作成し、実際に使用するためにデプロイした各種のアプリケーション分野のプロジェクトについて検討する。 使用する技術、適用の形式、得られた結果、そしてソフトウェア産業が形式的な検証技術やツールの恩恵を受ける能力について示すべき教訓を考察する。
  論文  参考訳（メタデータ） (2023-01-05T18:18:46Z)
• Fault-Aware Neural Code Rankers [64.41888054066861]
  サンプルプログラムの正しさを予測できる故障認識型ニューラルネットワークローダを提案する。 我々のフォールト・アウェア・ローダは、様々なコード生成モデルのpass@1精度を大幅に向上させることができる。
  論文  参考訳（メタデータ） (2022-06-04T22:01:05Z)
• A Formally Certified End-to-End Implementation of Shor's Factorization Algorithm [9.349616752756024]
  そこで我々はShorの素因数分解アルゴリズムのエンド・ツー・エンド実装を初めて公式に認定した。 私たちのフレームワークを活用することで、ヒューマンエラーの影響を著しく低減できます。
  論文  参考訳（メタデータ） (2022-04-14T17:02:34Z)

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

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