論文の概要: What Challenges Do Developers Face When Using Verification-Aware Programming Languages?
- arxiv url: http://arxiv.org/abs/2506.23696v1
- Date: Mon, 30 Jun 2025 10:17:39 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-07-01 21:27:54.014221
- 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とコンパイル時または実行時の形式的検証をサポートし、従来のテストよりも正確性を保証する。
- 参考スコア（独自算出の注目度）: 45.44831696628473
- 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言語のユーザビリティを改善し、検証ツールをより使いやすくするための実用的な洞察を提供する。
関連論文リスト
- 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) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。