論文の概要: Applying Formal Methods Tools to an Electronic Warfare Codebase (Experience report)

• arxiv url: http://arxiv.org/abs/2601.11510v1
• Date: Fri, 16 Jan 2026 18:46:19 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-01-19 20:21:50.602272
• Title: Applying Formal Methods Tools to an Electronic Warfare Codebase (Experience report)
• Title（参考訳）: 電子戦時コードベースへのフォーマルメソッドツールの適用(実験報告)
• Authors: Letitia W. Li, Denley Lam, Vu Le, Daniel Mitchell, Mark J. Gerken, Robert B. Ross,
• Abstract要約: 我々は,電子戦時(EW)システムに厳密な安全要件を持つ形式的手法を識別し,適用した経験について論じる。 本稿では,機能ドキュメンテーションの改善,手作業の削減,ライブラリコードの扱いの改善など,形式的メソッドのユーザビリティ向上を提案する。
• 参考スコア（独自算出の注目度）: 5.130336628792388
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: While using formal methods offers advantages over unit testing, their steep learning curve can be daunting to developers and can be a major impediment to widespread adoption. To support integration into an industrial software engineering workflow, a tool must provide useful information and must be usable with relatively minimal user effort. In this paper, we discuss our experiences associated with identifying and applying formal methods tools on an electronic warfare (EW) system with stringent safety requirements and present perspectives on formal methods tools from EW software engineers who are proficient in development yet lack formal methods training. In addition to a difference in mindset between formal methods and unit testing approaches, some formal methods tools use terminology or annotations that differ from their target programming language, creating another barrier to adoption. Input/output contracts, objects in memory affected by a function, and loop invariants can be difficult to grasp and use. In addition to usability, our findings include a comparison of vulnerabilities detected by different tools. Finally, we present suggestions for improving formal methods usability including better documentation of capabilities, decreased manual effort, and improved handling of library code.
• Abstract（参考訳）: 形式的なメソッドを使うことは、ユニットテストよりもメリットがありますが、彼らの急激な学習曲線は開発者を悩ませ、広く採用する上で大きな障害となり得るのです。 産業用ソフトウェアエンジニアリングワークフローへの統合をサポートするためには、ツールは有用な情報を提供しなければならない。 本稿では,電子戦争(EW)システムにおいて,厳密な安全要件を持つ形式的手法ツールを特定し,適用した経験について論じるとともに,形式的手法の訓練を欠いているEWソフトウェア技術者による形式的手法ツールの展望を紹介する。 形式的メソッドと単体テストアプローチの考え方の違いに加えて、いくつかの形式的メソッドは、ターゲットとするプログラミング言語とは異なる用語やアノテーションを使用し、採用の障壁をもう1つ生み出している。 入力/出力契約、関数に影響されたメモリ内のオブジェクト、ループ不変量は把握と使用が難しい。 ユーザビリティに加えて,さまざまなツールが検出した脆弱性の比較も行った。 最後に,機能ドキュメンテーションの改善,手作業の削減,ライブラリコードの扱いの改善など,形式的メソッドのユーザビリティ向上を提案する。

関連論文リスト

• Improving Large Language Models Function Calling and Interpretability via Guided-Structured Templates [56.73907811047611]
  大規模言語モデル(LLM)は強力な推論とツール使用能力を示している。 LLMは、誤ったパラメータ化、悪いツールの選択、ユーザーの意図の誤解釈によって、現実世界のツールインタラクションで失敗することが多い。 我々は、構造化推論テンプレートを利用して、関数呼び出しを生成するためのより故意なステップバイステップ命令を通してLCMをガイドするカリキュラムに着想を得たフレームワークを提案する。
  論文  参考訳（メタデータ） (2025-09-22T17:55:14Z)
• Alignment with Fill-In-the-Middle for Enhancing Code Generation [56.791415642365415]
  コードスニペットを小さな粒度のブロックに分割し,同じテストケースからより多様なDPOペアを生成する手法を提案する。 提案手法は,HumanEval (+), MBPP (+), APPS, LiveCodeBench, BigCodeBenchといったベンチマークデータセットの実験によって検証された,コード生成タスクの大幅な改善を示す。
  論文  参考訳（メタデータ） (2025-08-27T03:15:53Z)
• What Challenges Do Developers Face When Using Verification-Aware Programming Languages? [43.72088093637808]
  ソフトウェア開発では、ソフトウェア信頼性の増大はテストを伴うことが多い。 複雑でクリティカルなシステムでは、開発者はDesign by Contract(DbC)メソッドを使って、ソフトウェアコンポーネントが満たさなければならない正確な仕様を定義することができます。 VA(Verification-Aware)プログラミング言語は、DbCとコンパイル時または実行時の形式的検証をサポートし、従来のテストよりも正確性を保証する。
  論文  参考訳（メタデータ） (2025-06-30T10:17:39Z)
• Training Language Models to Generate Quality Code with Program Analysis Feedback [66.0854002147103]
  大規模言語モデル(LLM)によるコード生成は、ますます本番環境で採用されているが、コード品質の保証には失敗している。 実運用品質のコードを生成するためにLLMにインセンティブを与える強化学習フレームワークであるREALを提案する。
  論文  参考訳（メタデータ） (2025-05-28T17:57:47Z)
• Establishing tool support for a concept DSL [0.0]
  この論文は、自己完結的で再利用可能な概念単位を用いて、ソフトウェアシステムの振る舞いをモデル化するためのDSLであるConceptualを記述している。 提案された戦略は単純なコンパイラで実装され、開発者はプログラムの推論に既存の分析ツールにアクセスして利用することができる。
  論文  参考訳（メタデータ） (2025-03-07T09:18:31Z)
• ToolCoder: A Systematic Code-Empowered Tool Learning Framework for Large Language Models [81.12673534903979]
  ツール学習は、大規模な言語モデル(LLM)にとって、外部ツールとのインタラクションを通じて、複雑な現実世界のタスクを解決する重要な機能として登場した。 本稿では,ツール学習をコード生成タスクとして再編成する新しいフレームワークであるToolCoderを提案する。
  論文  参考訳（メタデータ） (2025-02-17T03:42:28Z)
• A Practical Approach to Formal Methods: An Eclipse Integrated Development Environment (IDE) for Security Protocols [0.33148826359547523]
  セキュリティプロトコルの設計、検証、実装のためのEclipse IDEを提示します。 モデル駆動開発アプローチの一部として、フォーマル化プロセスでユーザフレンドリな支援を提供する。
  論文  参考訳（メタデータ） (2024-11-26T22:44:08Z)
• Unified Pretraining Framework for Document Understanding [52.224359498792836]
  文書理解のための統合事前学習フレームワークであるUDocを紹介する。 UDocは、ほとんどのドキュメント理解タスクをサポートするように設計されており、Transformerを拡張してマルチモーダル埋め込みを入力とする。 UDocの重要な特徴は、3つの自己管理的損失を利用して汎用的な表現を学ぶことである。
  論文  参考訳（メタデータ） (2022-04-22T21:47:04Z)
• Modular approach to data preprocessing in ALOHA and application to a smart industry use case [0.0]
  データ前処理と変換パイプラインをサポートするために、ALOHAツールフローに統合されたモジュラーアプローチに対処する。 提案手法の有効性を示すために,キーワードスポッティングのユースケースに関する実験結果を示す。
  論文  参考訳（メタデータ） (2021-02-02T06:48:51Z)

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

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