論文の概要: MutDafny: A Mutation-Based Approach to Assess Dafny Specifications

• arxiv url: http://arxiv.org/abs/2511.15403v1
• Date: Wed, 19 Nov 2025 12:58:06 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-11-20 15:51:28.806234
• Title: MutDafny: A Mutation-Based Approach to Assess Dafny Specifications
• Title（参考訳）: MutDafny: Dafny仕様を評価するミューテーションベースのアプローチ
• Authors: Isabel Amaral, Alexandra Mendes, José Campos,
• Abstract要約: 潜在的な弱点を自動的に通知することで、Dafny仕様の信頼性を高めるツールであるMutDafnyを提示する。 一般的なツールから突然変異演算子を解析し、Dafnyに適用可能なものを同定する。 実世界の794個のDafnyプログラムのデータセットにおいて,MutDafnyの有効性と効率を評価する。
• 参考スコア（独自算出の注目度）: 46.0054630008219
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: This paper explores the use of mutation testing to reveal weaknesses in formal specifications written in Dafny. In verification-aware programming languages, such as Dafny, despite their critical role, specifications are as prone to errors as implementations. Flaws in specs can result in formally verified programs that deviate from the intended behavior. We present MutDafny, a tool that increases the reliability of Dafny specifications by automatically signaling potential weaknesses. Using a mutation testing approach, we introduce faults (mutations) into the code and rely on formal specifications for detecting them. If a program with a mutant verifies, this may indicate a weakness in the specification. We extensively analyze mutation operators from popular tools, identifying the ones applicable to Dafny. In addition, we synthesize new operators tailored for Dafny from bugfix commits in publicly available Dafny projects on GitHub. Drawing from both, we equipped our tool with a total of 32 mutation operators. We evaluate MutDafny's effectiveness and efficiency in a dataset of 794 real-world Dafny programs and we manually analyze a subset of the resulting undetected mutants, identifying five weak real-world specifications (on average, one at every 241 lines of code) that would benefit from strengthening.
• Abstract（参考訳）: 本稿では、Dafnyで書かれた形式仕様の弱点を明らかにするために、突然変異検査を用いる方法について検討する。 Dafnyのような検証対応のプログラミング言語では、その重要な役割にもかかわらず、仕様は実装と同じくらいエラーを起こしやすい。 仕様の欠陥は、意図された振る舞いから逸脱する、正式に検証されたプログラムをもたらす可能性がある。 潜在的な弱点を自動的に通知することで、Dafny仕様の信頼性を高めるツールであるMutDafnyを提示する。 突然変異テストアプローチを使用して、コードに障害(変更)を導入し、それを検出するための正式な仕様に依存します。 もしミュータントを持つプログラムが検証できれば、これは仕様の弱点を示すかもしれない。 一般的なツールから変異演算子を広範囲に解析し,Dafnyに適用可能なものを特定する。 さらに、GitHub上で公開されているDafnyプロジェクトのバグフィックスコミットから、Dafny用に調整された新しいオペレータを合成します。 両者の図面から,32個の突然変異演算子を具備した。 実世界の794のDafnyプログラムのデータセットにおいて、MutDafnyの有効性と効率を評価し、得られた未検出ミュータントのサブセットを手動で分析し、強化の恩恵を受ける5つの弱い実世界の仕様(平均241行毎のコード平均1つ)を特定した。

関連論文リスト

• Probing Pre-trained Language Models on Code Changes: Insights from ReDef, a High-Confidence Just-in-Time Defect Prediction Dataset [0.0]
  本稿では,22の大規模C/C++プロジェクトから得られた関数レベル修正の信頼性の高いベンチマークであるReDefを紹介する。 欠陥ケースはコミットの反転によって固定され、クリーンケースはポストホック履歴チェックによって検証される。 このパイプラインは3,164の欠陥と10,268のクリーンな修正をもたらし、既存のリソースよりも信頼性の高いラベルを提供する。
  論文  参考訳（メタデータ） (2025-09-11T07:07:11Z)
• Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs [79.74676890436174]
  本稿では,障害の局所化と修復のためのオラクルとして形式仕様を用いたDafny用のAPRツールを提案する。 プログラム内の各ステートメントの状態を決定するために、Hoareロジックの使用を含む一連のステップを通じて、障害をローカライズします。 また, GPT-4o miniが74.18%と高い修理成功率を示した。
  論文  参考訳（メタデータ） (2025-07-04T15:36:12Z)
• A Formally Verified Robustness Certifier for Neural Networks (Extended Version) [0.0]
  ニューラルネットワークは入力中の小さな摂動の影響を受けやすいため、それらが誤分類される。 グローバルなロバストニューラルネットワークは、入力の分類がそのような摂動によって変更できないことを証明するために機能を使用する。 本稿では,プログラムとその仕様,実装と検証に要する重要な設計決定について述べる。
  論文  参考訳（メタデータ） (2025-05-11T12:05:14Z)
• Automated Proof Generation for Rust Code via Self-Evolution [69.25795662658356]
  私たちは、Rustコードの自動証明生成を可能にする、人書きスニペットの欠如を克服するフレームワークであるSAFEを紹介します。 SAFEは、細調整されたモデルの自己老化能力を訓練するために、多数の合成不正確な証明を再利用する。 我々は、人間の専門家によるベンチマークで52.52%の精度で達成し、GPT-4oのパフォーマンス14.39%を大きく上回った。
  論文  参考訳（メタデータ） (2024-10-21T08:15:45Z)
• Automated Software Vulnerability Static Code Analysis Using Generative Pre-Trained Transformer Models [0.8192907805418583]
  生成事前学習トランスフォーマーモデルは、様々な自然言語処理タスクにおいて驚くほど効果的であることが示されている。 我々は,脆弱なコード構文の存在を自動的に識別するタスクにおいて,オープンソースのGPTモデルの有効性を評価する。
  論文  参考訳（メタデータ） (2024-07-31T23:33:26Z)

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

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