論文の概要: Enabling Unit Proofing for Software Implementation Verification

• arxiv url: http://arxiv.org/abs/2410.14818v1
• Date: Fri, 18 Oct 2024 18:37:36 GMT
• ステータス: 翻訳完了
• システム内更新日: 2024-10-22 13:19:55.967227
• Title: Enabling Unit Proofing for Software Implementation Verification
• Title（参考訳）: ソフトウェア実装検証のための単体証明の実施
• Authors: Paschal C. Amusuo, Parth V. Patil, Owen Cochell, Taylor Le Lievre, James C. Davis,
• Abstract要約: 本稿では,方法論とツールの両面から,単体証明フレームワークの研究課題を提案する。 これにより、エンジニアはコードレベルの欠陥を早期に発見できる。
• 参考スコア（独自算出の注目度）: 2.7325338323814328
• License:
• 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のユニット検証の使用を調査し、現在のアプローチが手作業であり、深刻な欠陥を隠蔽する欠陥があることを示した。 本稿では,ソフトウェア技術者が効果的かつ効率的にユニット検証を行うことを支援するための,手法とツールの両面から,ユニット検証フレームワークの研究課題を提案する。 これにより、エンジニアはコードレベルの欠陥を早期に発見できる。

関連論文リスト

• Verifying Non-friendly Formal Verification Designs: Can We Start Earlier? [2.1626093085892144]
  本稿では,2つの主要なステップからなるメタモデリング技術に基づく自動手法を提案する。 まず、C++で書かれた未使用のアルゴリズム記述を、生成されたアサーションを使用して早期に検証する。 第2に、HLECとそのメタモデルパラメータを用いて、このアルゴリズム記述をシーケンシャルな設計に対して検証する。
  論文  参考訳（メタデータ） (2024-10-24T06:09:40Z)
• 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)

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

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