論文の概要: What Challenges Do Developers Face When Using Verification-Aware Programming Languages?
- arxiv url: http://arxiv.org/abs/2506.23696v2
- Date: Sun, 07 Sep 2025 11:10:45 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-09-09 14:07:03.157094
- Title: What Challenges Do Developers Face When Using Verification-Aware Programming Languages?
- Title（参考訳）: 検証対応プログラミング言語を使用する場合、開発者はどのような課題に直面するのか?
- Authors: Francisco Oliveira, Alexandra Mendes, Carolina Carreira,
- Abstract要約: ソフトウェア開発では、ソフトウェア信頼性の増大はテストを伴うことが多い。
複雑でクリティカルなシステムでは、開発者はDesign by Contract(DbC)メソッドを使って、ソフトウェアコンポーネントが満たさなければならない正確な仕様を定義することができます。
VA(Verification-Aware)プログラミング言語は、DbCとコンパイル時または実行時の形式的検証をサポートし、従来のテストよりも正確性を保証する。
- 参考スコア（独自算出の注目度）: 43.72088093637808
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Software reliability is critical in ensuring that the digital systems we depend on function correctly. In software development, increasing software reliability often involves testing. However, for complex and critical systems, developers can use Design by Contract (DbC) methods to define precise specifications that software components must satisfy. Verification-Aware (VA) programming languages support DbC and formal verification at compile-time or run-time, offering stronger correctness guarantees than traditional testing. However, despite the strong guarantees provided by VA languages, their adoption remains limited. In this study, we investigate the barriers to adopting VA languages by analyzing developer discussions on public forums using topic modeling techniques. We complement this analysis with a developer survey to better understand the practical challenges associated with VA languages. Our findings reveal key obstacles to adoption, including steep learning curves and usability issues. Based on these insights, we identify actionable recommendations to improve the usability and accessibility of VA languages. Our findings suggest that simplifying tool interfaces, providing better educational materials, and improving integration with everyday development environments could improve the usability and adoption of these languages. Our work provides actionable insights for improving the usability of VA languages and making verification tools more accessible.
- Abstract（参考訳）: ソフトウェア信頼性は、私たちが機能に依存しているデジタルシステムが正しく機能することを保証するために重要である。
ソフトウェア開発では、ソフトウェア信頼性の増大はテストを伴うことが多い。
しかし、複雑でクリティカルなシステムでは、開発者はDesign by Contract(DbC)メソッドを使って、ソフトウェアコンポーネントが満たさなければならない正確な仕様を定義することができます。
VA(Verification-Aware)プログラミング言語は、DbCとコンパイル時または実行時の形式的検証をサポートし、従来のテストよりも正確性を保証する。
しかし、VA言語による強い保証にもかかわらず、その採用は限られている。
本研究では,トピックモデリング技術を用いたパブリックフォーラムにおける開発者の議論を分析し,VA言語導入の障壁について検討する。
この分析を開発者調査で補完し,VA言語に関連する実践的課題をより深く理解する。
この結果から,学習曲線の急激さやユーザビリティの問題など,採用の大きな障害が明らかになった。
これらの知見に基づき、VA言語のユーザビリティとアクセシビリティを向上させるために実行可能なレコメンデーションを特定する。
この結果から,ツールインタフェースの簡素化,教育教材の充実,日常開発環境との統合性の向上が,これらの言語の利用性や採用性の向上につながることが示唆された。
我々の研究は、VA言語のユーザビリティを改善し、検証ツールをより使いやすくするための実用的な洞察を提供する。
関連論文リスト
- Applying Formal Methods Tools to an Electronic Warfare Codebase (Experience report) [5.130336628792388]
我々は,電子戦時(EW)システムに厳密な安全要件を持つ形式的手法を識別し,適用した経験について論じる。
本稿では,機能ドキュメンテーションの改善,手作業の削減,ライブラリコードの扱いの改善など,形式的メソッドのユーザビリティ向上を提案する。
論文 参考訳（メタデータ） (2026-01-16T18:46:19Z) - SV-LIB 1.0: A Standard Exchange Format for Software-Verification Tasks [2.5374060352463697]
SV-LIBはソフトウェア検証タスクのための交換形式と中間言語である。
本稿では,SV-LIBformatのバージョン1.0について述べる。
論文 参考訳（メタデータ） (2025-11-26T15:44:54Z) - Improving Large Language Models Function Calling and Interpretability via Guided-Structured Templates [56.73907811047611]
大規模言語モデル(LLM)は強力な推論とツール使用能力を示している。
LLMは、誤ったパラメータ化、悪いツールの選択、ユーザーの意図の誤解釈によって、現実世界のツールインタラクションで失敗することが多い。
我々は、構造化推論テンプレートを利用して、関数呼び出しを生成するためのより故意なステップバイステップ命令を通してLCMをガイドするカリキュラムに着想を得たフレームワークを提案する。
論文 参考訳（メタデータ） (2025-09-22T17:55:14Z) - On Integrating Large Language Models and Scenario-Based Programming for Improving Software Reliability [2.2058293096044586]
大規模言語モデル(LLM)は、ソフトウェア開発者にとって急速に欠かせないツールになりつつある。
LLMは、しばしば重大なエラーを導入し、説得力のある信頼を持って間違ったコードを提示する。
本研究では,LLMと従来のソフトウェア工学技術を組み合わせる手法を構造化された方法で提案する。
論文 参考訳（メタデータ） (2025-09-11T07:10:25Z) - Evaluating Language Model Reasoning about Confidential Information [95.64687778185703]
言語モデルが文脈的堅牢性を示すか、文脈依存型安全仕様に準拠する能力を示すかを検討する。
我々は,ユーザ要求がいつ承認されたか,言語モデルが正しく判断できるかどうかを測定するベンチマーク(PasswordEval)を開発した。
現在のオープンソースとクローズドソースのモデルでは、一見単純な作業に苦労しています。
論文 参考訳（メタデータ） (2025-08-27T15:39:46Z) - NEAT: QCP: A Practical Separation Logic-based C Program Verification Tool [4.449417653464987]
本稿では,textbf C Programming Verifier (QCP) と呼ばれる新しい検証ツールを紹介する。
QCPは、ユーザインタラクションを強化するために、アサーション言語の洗練されたフロントエンド%シンタクスを組み込んでいる。
論文 参考訳（メタデータ） (2025-05-19T09:04:34Z) - Development and Adoption of SATD Detection Tools: A State-of-practice Report [5.670597842524448]
Self-Admitted Technical Debt (SATD)は、開発者が故意に最適化されたソリューションをコードに導入するインスタンスを指す。
本稿では,SATD検出ツールの開発と導入に関する総合的な状況報告を提供する。
論文 参考訳（メタデータ） (2024-12-18T12:06:53Z) - Training of Scaffolded Language Models with Language Supervision: A Survey [62.59629932720519]
本調査は,戦後のLM周辺における新規構造物の設計と最適化に関する文献を整理した。
本稿では,この階層構造を足場型LMと呼び,ツールを用いた多段階プロセスに統合されたLMに焦点を当てる。
論文 参考訳（メタデータ） (2024-10-21T18:06:25Z) - Multilingual Crowd-Based Requirements Engineering Using Large Language Models [9.93427497289912]
私たちは、アジャイルチームが問題やタスク管理にクラウドベースの要件エンジニアリング(CrowdRE)を使用するのを支援するLLMベースのアプローチを提示します。
現在私たちは、開発者が関連するユーザレビューと問題にマッチできるコマンドラインツールを実装しています。
論文 参考訳（メタデータ） (2024-08-12T21:40:39Z) - DIALIGHT: Lightweight Multilingual Development and Evaluation of
Task-Oriented Dialogue Systems with Large Language Models [76.79929883963275]
DIALIGHTは多言語タスク指向対話(ToD)システムの開発と評価のためのツールキットである。
ローカル発話レベルとグローバル対話レベルの両方において、人間のきめ細かい評価のためのセキュアでユーザフレンドリーなWebインターフェースを備えている。
評価の結果, PLMの微調整により精度とコヒーレンスが向上する一方, LLMベースのシステムは多様で類似した応答を生成するのに優れていた。
論文 参考訳（メタデータ） (2024-01-04T11:27:48Z) - AdaCCD: Adaptive Semantic Contrasts Discovery Based Cross Lingual
Adaptation for Code Clone Detection [69.79627042058048]
AdaCCDは、その言語でアノテーションを使わずに、新しい言語のクローンコードを検出する新しい言語間適応手法である。
5つのプログラミング言語からなる多言語コードクローン検出ベンチマークを構築し,AdaCCDの言語間適応性を評価する。
論文 参考訳（メタデータ） (2023-11-13T12:20:48Z) - ChatDev: Communicative Agents for Software Development [84.90400377131962]
ChatDevはチャットを利用したソフトウェア開発フレームワークで、特別なエージェントがコミュニケーション方法についてガイドされる。
これらのエージェントは、統一された言語ベースのコミュニケーションを通じて、設計、コーディング、テストフェーズに積極的に貢献する。
論文 参考訳（メタデータ） (2023-07-16T02:11:34Z) - AIBugHunter: A Practical Tool for Predicting, Classifying and Repairing
Software Vulnerabilities [27.891905729536372]
AIBugHunterは、C/C++言語用のMLベースのソフトウェア脆弱性分析ツールで、Visual Studio Codeに統合されている。
本稿では,新たな多目的最適化(MOO)に基づく脆弱性分類手法と,AIBugHunterが脆弱性タイプを正確に識別し,重症度を推定するためのトランスフォーマーに基づく評価手法を提案する。
論文 参考訳（メタデータ） (2023-05-26T04:21:53Z) - MLSmellHound: A Context-Aware Code Analysis Tool [4.157846027410602]
コード分析ツールは、複数のプログラミング言語として表されるチーム内の文化的な違いを考慮に入れなければならない。
既存のツールはこれらの文化的な違いを識別できず、機械学習プロジェクトへの採用を減らすソフトウェアエンジニアリングに向けられている。
このアプローチでは、ソースコードの目的(i)技術ドメイン(iii)問題ドメイン(iv)チームノルム(v)開発ライフサイクルステージを含むコンテキストの利用を探索し、この問題を解決しようと試みています。
これにより、エンドユーザーに対してコンテキスト化された意味のあるエラーレポートが可能になる。
論文 参考訳（メタデータ） (2022-05-08T06:01:22Z) - AVATAR: A Parallel Corpus for Java-Python Program Translation [77.86173793901139]
プログラム翻訳とは、ある言語から別の言語へソースコードを移行することを指す。
AVATARは9,515のプログラミング問題とそのソリューションをJavaとPythonという2つの人気のある言語で記述したものです。
論文 参考訳（メタデータ） (2021-08-26T05:44:20Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。