論文の概要: Combining Tests and Proofs for Better Software Verification

• arxiv url: http://arxiv.org/abs/2601.16239v1
• Date: Wed, 21 Jan 2026 22:39:17 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-01-26 14:27:27.357726
• Title: Combining Tests and Proofs for Better Software Verification
• Title（参考訳）: より良いソフトウェア検証のためのテストと証明を組み合わせる
• Authors: Li Huang, Bertrand Meyer, Manuel Oriol,
• Abstract要約: 検証された品質のソフトウェアを作るための競合する技術よりも、テストと証明が相補的である、という異なる視点が生まれています。 逆例はプログラムをフェールさせる入力の組み合わせである。 しかし、自動テスト生成のツールとして、不正なプログラムに反例生成を適用することができる。 これらのメカニズムは、修正が正しいことを保証しながら、不正なプログラムのプログラム修正を作成するのに役立ちます。
• 参考スコア（独自算出の注目度）: 30.905701881162685
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Test or prove? These two approaches to software verification have long been presented as opposites. One is dynamic, the other static: a test executes the program, a proof only analyzes the program text. A different perspective is emerging, in which testing and proving are complementary rather than competing techniques for producing software of verified quality. Work performed over the past few years and reviewed here develops this complementarity by taking advantage of Design by Contract, as available in Eiffel, and exploiting a feature of modern program-proving tools based on ``Satisfiability Modulo Theories'' (SMT): counterexample generation. A counterexample is an input combination that makes the program fail. If we are trying to prove a program correct, we hope not to find any. One can, however, apply counterexample generation to incorrect programs, as a tool for automatic test generation. We can also introduce faults into a correct program and turn the counterexamples into an automatically generated regression test suite with full coverage. Additionally, we can use these mechanisms to help produce program fixes for incorrect programs, with a guarantee that the fixes are correct. All three applications, leveraging on the mechanisms of Eiffel and Design by Contract, hold significant promise to address some of the challenges of program testing, software maintenance and Automatic Program Repair.
• Abstract（参考訳）: テストか、それとも証明か? ソフトウェア検証に対するこれらの2つのアプローチは、長い間逆として提示されてきた。 1つは動的で、もう1つは静的で、テストはプログラムを実行し、証明はプログラムのテキストのみを分析する。 検証された品質のソフトウェアを作るための競合する技術よりも、テストと証明が相補的である、という異なる視点が生まれています。 Eiffel で利用可能な Design by Contract を利用して,‘Satisfiability Modulo Theories' (SMT)’ に基づいた現代的なプログラム実装ツールの機能を活用することで,この相補性を開発した。 逆例はプログラムをフェールさせる入力の組み合わせである。 プログラムの正しさを証明しようとするなら、何も見つからないことを願っています。 しかし、自動テスト生成のツールとして、不正なプログラムに反例生成を適用することができる。 また、障害を正しいプログラムに導入して、反例を完全なカバレッジを備えた自動生成された回帰テストスイートに変換することもできます。 さらに、これらのメカニズムを使用して、修正が正しいことを保証しながら、不正なプログラムのプログラム修正を作成することができる。 EiffelとDesign by Contractのメカニズムを活用する3つのアプリケーションはいずれも,プログラムテストやソフトウェアメンテナンス,自動プログラム修正といった課題に対処する,という大きな約束を持っています。

関連論文リスト

• Do AI models help produce verified bug fixes? [62.985237003585674]
  大規模言語モデルは、ソフトウェアバグの修正に使用される。 本稿では,プログラマが大規模言語モデルを用いて,自身のスキルを補完する方法について検討する。 その結果は、プログラムバグに対する保証された修正を提供するAIとLLMの適切な役割への第一歩となる。
  論文  参考訳（メタデータ） (2025-07-21T17:30:16Z)
• 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 Unit Proofing Framework for Code-level Verification: A Research Agenda [2.7325338323814328]
  本稿では,方法論とツールの両面から,単体証明フレームワークの研究課題を提案する。 これにより、エンジニアはコードレベルの欠陥を早期に発見できる。
  論文  参考訳（メタデータ） (2024-10-18T18:37:36Z)
• Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming [8.34623776815378]
  我々は600K行のオープンソースF*プログラムと証明のデータセットをキュレートする。 このデータセットには、Windows、Linux、Python、Firefoxなど、プロダクションシステムで使用されるソフトウェアが含まれている。 我々は,AIを用いてプログラムとその証明をF*で合成し,有望な結果を得る。
  論文  参考訳（メタデータ） (2024-05-03T00:14:33Z)
• Retromorphic Testing: A New Approach to the Test Oracle Problem [4.183247207161993]
  テストオラクルは、ソフトウェア出力と所定の入力セットの予測動作との対応を評価するための基準またはメカニズムとして機能する。 逆関数の数学的概念に着想を得て,新しいブラックボックステスト手法であるRetromorphic Testingを提案する。 本稿では,アルゴリズム,従来のソフトウェア,AIアプリケーションなど,さまざまなプログラムにまたがる実例を用いた3つのテストモードを提案する。
  論文  参考訳（メタデータ） (2023-10-10T09:03:01Z)
• NAPG: Non-Autoregressive Program Generation for Hybrid Tabular-Textual Question Answering [52.10214317661547]
  現在の数値推論法はプログラムシーケンスを自己回帰的にデコードする。 プログラム生成の精度は、デコードステップがエラー伝搬によって展開されるにつれて急激に低下する。 本稿では,非自己回帰型プログラム生成フレームワークを提案する。
  論文  参考訳（メタデータ） (2022-11-07T11:25:21Z)
• Fault-Aware Neural Code Rankers [64.41888054066861]
  サンプルプログラムの正しさを予測できる故障認識型ニューラルネットワークローダを提案する。 我々のフォールト・アウェア・ローダは、様々なコード生成モデルのpass@1精度を大幅に向上させることができる。
  論文  参考訳（メタデータ） (2022-06-04T22:01:05Z)
• Learning from Self-Sampled Correct and Partially-Correct Programs [96.66452896657991]
  そこで本研究では,モデルが学習中にサンプリングを行い,自己サンプリングされた完全正当プログラムと部分正当プログラムの両方から学習することを提案する。 自己サンプリング型プログラムと部分修正型プログラムを併用することで,学習とサンプリングプロセスのガイドに役立てることができることを示す。 提案手法は,MLEを用いた単一の参照プログラムからの学習と比較して,パス@kの性能を3.1%から12.3%向上させる。
  論文  参考訳（メタデータ） (2022-05-28T03:31:07Z)

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

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