論文の概要: 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を提案する。
関連論文リスト
- Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification [15.686651364655958]
AutoSpecは、自動プログラム検証のための仕様を合成するための自動化アプローチである。
仕様の汎用性における既存の作業の欠点を克服し、完全な証明のために十分かつ適切な仕様を合成する。
実世界のX509パーサプロジェクトでプログラムを検証するためにうまく適用することができる。
論文 参考訳(メタデータ) (2024-03-31T18:15:49Z) - Trustworthy Distributed Certification of Program Execution [2.208443815105053]
我々は,モナと呼ばれるプロトタイププログラミング言語と認証プロトコルOCCPを組み合わせた,革新的なアプローチを提案する。
本プロトコルでは,再実行を素直に行うことなく,プログラムセグメントを分散し,不変かつ信頼性の高いシステムで認証することができる。
本研究は,既存の最先端手法と比較してプログラム実行回数を減らす手法の有効性を示すものである。
論文 参考訳(メタデータ) (2024-02-21T13:21:37Z) - Selene: Pioneering Automated Proof in Software Verification [69.7891799471749]
我々は,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 Verification Framework for Dynamical and Control Models via
Certificate Synthesis [60.03938402120854]
システム仕様を符号化し、対応する証明書を定義するためのフレームワークを提供する。
コントローラと証明書を形式的に合成する自動化手法を提案する。
我々のアプローチは、ニューラルネットワークの柔軟性を利用して、制御のための安全な学習の幅広い分野に寄与する。
論文 参考訳(メタデータ) (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) - Analyzing Maintenance Activities of Software Libraries [65.268245109828]
近年、産業アプリケーションはオープンソースソフトウェアライブラリを深く統合している。
産業アプリケーションに対する自動監視アプローチを導入して、オープンソース依存関係を特定し、その現状や将来的なメンテナンス活動に関するネガティブな兆候を示したいと思っています。
論文 参考訳(メタデータ) (2023-06-09T16:51:25Z) - Automatic Program Instrumentation for Automatic Verification (Extended
Technical Report) [0.0]
帰納的検証とソフトウェアモデルチェックでは、特定の仕様言語構造を扱うことが問題となる。
本稿では,様々なアドホックなアプローチを仮定する統一検証パラダイムとして,インスツルメンテーションを提案する。
我々は,プログラムのアグリゲーションによる検証に適したMonoCeraツールにアプローチを実装した。
論文 参考訳(メタデータ) (2023-05-26T14:55:35Z) - Rethinking Certification for Trustworthy Machine Learning-Based
Applications [3.886429361348165]
機械学習(ML)は、非決定論的振る舞いを持つ高度なアプリケーションの実装にますます使われています。
既存の認証スキームは、MLモデル上に構築された非決定論的アプリケーションにはすぐには適用されない。
本稿では、現状の認定制度の課題と欠陥を分析し、オープンな研究課題について論じ、MLベースのアプリケーションのための最初の認定制度を提案する。
論文 参考訳(メタデータ) (2023-05-26T11:06:28Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。