論文の概要: Klever: Verification Framework for Critical Industrial C Programs

• arxiv url: http://arxiv.org/abs/2309.16427v1
• Date: Thu, 28 Sep 2023 13:23:59 GMT
• ステータス: 処理完了
• システム内更新日: 2023-10-23 06:08:15.766962
• Title: Klever: Verification Framework for Critical Industrial C Programs
• Title（参考訳）: Klever: 重要な産業用Cプログラムの検証フレームワーク
• Authors: Ilja Zakharov, Evgeny Novikov, Ilya Shchepetkov
• Abstract要約: 我々は,大規模かつ重要な産業用Cプログラムに自動ソフトウェア検証ツールを適用する労力を削減するために,Kleverソフトウェア検証フレームワークを提案する。 既存のツールは、環境モデリング、要件の仕様、ターゲットプログラムの多くのバージョンと構成の検証、検証結果のエキスパートアセスメントなど、広く採用されている手段を提供していない。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Automatic software verification tools help to find hard-to-detect faults in programs checked against specified requirements non-interactively. Besides, they can prove program correctness formally under certain assumptions. These capabilities are vital for verification of critical industrial programs like operating system kernels and embedded software. However, such programs can contain hundreds or thousands of KLOC that prevent obtaining valuable verification results in any reasonable time when checking non-trivial requirements. Also, existing tools do not provide widely adopted means for environment modeling, specification of requirements, verification of many versions and configurations of target programs, and expert assessment of verification results. In this paper, we present the Klever software verification framework, designed to reduce the effort of applying automatic software verification tools to large and critical industrial C programs.
• Abstract（参考訳）: 自動ソフトウェア検証ツールは、特定の要求に対して非インタラクティブにチェックされたプログラムの障害を検出するのに役立ちます。 さらに、特定の仮定の下でプログラムの正確性を証明することもできる。 これらの機能は、オペレーティングシステムカーネルや組み込みソフトウェアのような重要な産業プログラムの検証に不可欠である。 しかしながら、このようなプログラムには数百から数千のKLOCが含まれており、非自明な要求をチェックするときに妥当な時間内に有効な検証結果を得ることができない。 また、既存のツールは、環境モデリング、要求仕様の特定、ターゲットプログラムの多くのバージョンと構成の検証、検証結果のエキスパート評価など、広く採用されている手段を提供していない。 本稿では,大規模かつ重要な産業用cプログラムに自動ソフトウェア検証ツールを適用する労力を削減するために設計されたklever software verification frameworkを提案する。

関連論文リスト

• Enabling Unit Proofing for Software Implementation Verification [2.7325338323814328]
  本稿では,方法論とツールの両面から,単体証明フレームワークの研究課題を提案する。 これにより、エンジニアはコードレベルの欠陥を早期に発見できる。
  論文  参考訳（メタデータ） (2024-10-18T18:37:36Z)
• The Impact of SBOM Generators on Vulnerability Assessment in Python: A Comparison and a Novel Approach [56.4040698609393]
  Software Bill of Materials (SBOM) は、ソフトウェア構成における透明性と妥当性を高めるツールとして推奨されている。 現在のSBOM生成ツールは、コンポーネントや依存関係を識別する際の不正確さに悩まされることが多い。 提案するPIP-sbomは,その欠点に対処する新しいピップインスパイアされたソリューションである。
  論文  参考訳（メタデータ） (2024-09-10T10:12:37Z)
• Towards Quantifying Requirements Technical Debt for Software Requirements concerning Veracity: A Perspective and Research Roadmap [3.763215468259125]
  我々はRTDのレンズを精度に関するソフトウェア要件に適用するための視点とビジョンを提示する。 我々のゴールは、重要な関心事としての妥当性の認識を育成し、最終的に、正確性に関するソフトウェア要件に対するRTDの管理を支援することである。
  論文  参考訳（メタデータ） (2024-06-29T10:10:03Z)
• Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification [15.686651364655958]
  AutoSpecは、自動プログラム検証のための仕様を合成するための自動化アプローチである。 仕様の汎用性における既存の作業の欠点を克服し、完全な証明のために十分かつ適切な仕様を合成する。 実世界のX509パーサプロジェクトでプログラムを検証するためにうまく適用することができる。
  論文  参考訳（メタデータ） (2024-03-31T18:15:49Z)
• Selene: Pioneering Automated Proof in Software Verification [62.09555413263788]
  実世界の産業レベルのマイクロカーネルであるseL4をベースとした,最初のプロジェクトレベルの自動証明ベンチマークであるSeleneを紹介する。 GPT-3.5-turbo や GPT-4 のような先進的な大規模言語モデル (LLM) による実験結果から, 自動証明生成領域における LLM の機能を強調した。
  論文  参考訳（メタデータ） (2024-01-15T13:08:38Z)
• Finding Software Vulnerabilities in Open-Source C Projects via Bounded Model Checking [2.9129603096077332]
  我々は,汎用ソフトウェアシステムの脆弱性を効果的に検出できる境界モデル検査手法を提唱する。 我々は,最先端の有界モデルチェッカーを用いて,大規模ソフトウェアシステムを検証する手法を開発し,評価した。
  論文  参考訳（メタデータ） (2023-11-09T11:25:24Z)
• A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis [54.959571890098786]
  システム仕様を符号化し、対応する証明書を定義するためのフレームワークを提供する。 コントローラと証明書を形式的に合成する自動化手法を提案する。 我々のアプローチは、ニューラルネットワークの柔軟性を利用して、制御のための安全な学習の幅広い分野に寄与する。
  論文  参考訳（メタデータ） (2023-09-12T09:37:26Z)
• Using Machine Learning To Identify Software Weaknesses From Software Requirement Specifications [49.1574468325115]
  本研究は、要求仕様からソフトウェア弱点を特定するための効率的な機械学習アルゴリズムを見つけることに焦点を当てる。 ProMISE_exp. Naive Bayes、サポートベクターマシン(SVM)、決定木、ニューラルネットワーク、畳み込みニューラルネットワーク(CNN)アルゴリズムをテストした。
  論文  参考訳（メタデータ） (2023-08-10T13:19:10Z)
• Automatic Program Instrumentation for Automatic Verification (Extended Technical Report) [0.0]
  帰納的検証とソフトウェアモデルチェックでは、特定の仕様言語構造を扱うことが問題となる。 本稿では,様々なアドホックなアプローチを仮定する統一検証パラダイムとして,インスツルメンテーションを提案する。 我々は,プログラムのアグリゲーションによる検証に適したMonoCeraツールにアプローチを実装した。
  論文  参考訳（メタデータ） (2023-05-26T14:55:35Z)
• Lessons from Formally Verified Deployed Software Systems (Extended version) [65.69802414600832]
  本稿は、正式に認証されたシステムを作成し、実際に使用するためにデプロイした各種のアプリケーション分野のプロジェクトについて検討する。 使用する技術、適用の形式、得られた結果、そしてソフトウェア産業が形式的な検証技術やツールの恩恵を受ける能力について示すべき教訓を考察する。
  論文  参考訳（メタデータ） (2023-01-05T18:18:46Z)
• Fault-Aware Neural Code Rankers [64.41888054066861]
  サンプルプログラムの正しさを予測できる故障認識型ニューラルネットワークローダを提案する。 我々のフォールト・アウェア・ローダは、様々なコード生成モデルのpass@1精度を大幅に向上させることができる。
  論文  参考訳（メタデータ） (2022-06-04T22:01:05Z)

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

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