論文の概要: Lessons from Formally Verified Deployed Software Systems (Extended version)
- arxiv url: http://arxiv.org/abs/2301.02206v3
- Date: Thu, 28 Mar 2024 22:01:48 GMT
- ステータス: 処理完了
- システム内更新日: 2024-04-01 21:06:09.761100
- Title: Lessons from Formally Verified Deployed Software Systems (Extended version)
- Title（参考訳）: 形式的に検証されたデプロイされたソフトウェアシステムから学んだこと(拡張バージョン)
- Authors: Li Huang, Sophie Ebersold, Alexander Kogtenkov, Bertrand Meyer, Yinling Liu,
- Abstract要約: 本稿は、正式に認証されたシステムを作成し、実際に使用するためにデプロイした各種のアプリケーション分野のプロジェクトについて検討する。
使用する技術、適用の形式、得られた結果、そしてソフトウェア産業が形式的な検証技術やツールの恩恵を受ける能力について示すべき教訓を考察する。
- 参考スコア（独自算出の注目度）: 65.69802414600832
- License: http://creativecommons.org/licenses/by-nc-sa/4.0/
- Abstract: The technology of formal software verification has made spectacular advances, but how much does it actually benefit the development of practical software? Considerable disagreement remains about the practicality of building systems with mechanically-checked proofs of correctness. Is this prospect confined to a few expensive, life-critical projects, or can the idea be applied to a wide segment of the software industry? To help answer this question, the present survey examines a range of projects, in various application areas, that have produced formally verified systems and deployed them for actual use. It considers the technologies used, the form of verification applied, the results obtained, and the lessons that the software industry should draw regarding its ability to benefit from formal verification techniques and tools. Note: this version is the extended article, covering all the systems identified as relevant. A shorter version, covering only a selection, is also available.
- Abstract（参考訳）: フォーマルなソフトウェア検証の技術は目覚ましい進歩を遂げましたが、実際のソフトウェアの開発にはどの程度の恩恵がありますか?
機械的検査による正当性証明による建築システムの実用性については、重要な意見の相違が残っている。
この見通しは、高価でライフクリティカルなプロジェクトに限定されているのだろうか、それとも、このアイデアをソフトウェア産業の広範囲に適用できるのだろうか?
本研究は, 各種のアプリケーション領域において, 公式に検証されたシステムを作成し, 実際に使用するためにデプロイしたプロジェクトについて検討する。
使用される技術、適用の形式、得られた結果、そしてソフトウェア産業が形式的な検証技術やツールの恩恵を受ける能力について示すべき教訓を考察する。
注意:このバージョンは拡張された記事であり、関連するものとして特定されたすべてのシステムをカバーする。
選択のみをカバーした短いバージョンも利用可能である。
関連論文リスト
- Enabling Unit Proofing for Software Implementation Verification [2.7325338323814328]
本稿では,方法論とツールの両面から,単体証明フレームワークの研究課題を提案する。
これにより、エンジニアはコードレベルの欠陥を早期に発見できる。
論文 参考訳（メタデータ） (2024-10-18T18:37:36Z) - Codev-Bench: How Do LLMs Understand Developer-Centric Code Completion? [60.84912551069379]
Code-Development Benchmark (Codev-Bench)は、細粒度で現実世界、リポジトリレベル、開発者中心の評価フレームワークです。
Codev-Agentは、リポジトリのクローリングを自動化し、実行環境を構築し、既存のユニットテストから動的呼び出しチェーンを抽出し、データ漏洩を避けるために新しいテストサンプルを生成するエージェントベースのシステムである。
論文 参考訳（メタデータ） (2024-10-02T09:11:10Z) - Estimating the Energy Footprint of Software Systems: a Primer [56.200335252600354]
ソフトウェアシステムのエネルギーフットプリントの定量化は、最も基本的な活動の1つです。
この文書は、この分野で研究を始めたい研究者の出発点となることを目的としている。
論文 参考訳（メタデータ） (2024-07-16T11:21:30Z) - Quantifying Software Correctness by Combining Architecture Modeling and
Formal Program Analysis [41.375461087536294]
QuACは、サービス指向ソフトウェアシステムの正しさを定量化するモジュラーアプローチである。
本稿では,モデリングツールPalladioと推論検証ツールKeYを用いたJava用QuACの実装について述べる。
論文 参考訳（メタデータ） (2024-01-25T17:18:33Z) - Charting a Path to Efficient Onboarding: The Role of Software
Visualization [49.1574468325115]
本研究は,ソフトウェアビジュアライゼーションツールを用いたマネージャ,リーダ,開発者の親しみやすさを探求することを目的としている。
本手法は, 質問紙調査と半構造化面接を用いて, 実践者から収集したデータの量的, 質的分析を取り入れた。
論文 参考訳（メタデータ） (2024-01-17T21:30:45Z) - Finding Software Vulnerabilities in Open-Source C Projects via Bounded
Model Checking [2.9129603096077332]
我々は,汎用ソフトウェアシステムの脆弱性を効果的に検出できる境界モデル検査手法を提唱する。
我々は,最先端の有界モデルチェッカーを用いて,大規模ソフトウェアシステムを検証する手法を開発し,評価した。
論文 参考訳（メタデータ） (2023-11-09T11:25:24Z) - End-of-Life of Software How is it Defined and Managed? [1.370633147306388]
古いソフトウェアを捨てて、急速に変化するニーズと要求を満たす新しいソフトウェアを取得するのは、より迅速かつ安価になってきている。
本稿では,ソフトウェアにおけるエンド・オブ・ライフのシステム工学的概念について考察する。
廃止を試みて放棄されたソフトウェアの例を先送りし、放棄されたソフトウェアアーティファクトの反感を探求する。
論文 参考訳（メタデータ） (2022-04-08T01:15:02Z) - Empowered and Embedded: Ethics and Agile Processes [60.63670249088117]
私たちは倫理的考慮事項を(アジャイル)ソフトウェア開発プロセスに組み込む必要があると論じています。
私たちは、すでに存在しており、確立されたアジャイルソフトウェア開発プロセスで倫理的な議論を実施する可能性を強調しました。
論文 参考訳（メタデータ） (2021-07-15T11:14:03Z) - A Review of Formal Methods applied to Machine Learning [0.6853165736531939]
機械学習システムの検証の新たな分野に適用される最先端の形式的手法を検討します。
我々はまず,安全クリティカルな分野であるavionic softwareにおいて確立された形式的手法とその現状を思い出す。
次に、機械学習のためにこれまでに開発された形式的手法を包括的かつ詳細にレビューし、その強みと限界を強調します。
論文 参考訳（メタデータ） (2021-04-06T12:48:17Z) - Machine Learning for Software Engineering: A Systematic Mapping [73.30245214374027]
ソフトウェア開発業界は、現代のソフトウェアシステムを高度にインテリジェントで自己学習システムに移行するために、機械学習を急速に採用している。
ソフトウェアエンジニアリングライフサイクルの段階にわたって機械学習の採用について、現状を探求する包括的な研究は存在しない。
本研究は,機械学習によるソフトウェア工学(MLSE)分類を,ソフトウェア工学ライフサイクルのさまざまな段階に適用性に応じて,最先端の機械学習技術に分類するものである。
論文 参考訳（メタデータ） (2020-05-27T11:56:56Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。