Fugu-MT 論文翻訳(概要): Interval Analysis in Industrial-Scale BMC Software Verifiers: A Case Study

論文の概要: Interval Analysis in Industrial-Scale BMC Software Verifiers: A Case Study

arxiv url: http://arxiv.org/abs/2406.15281v1
Date: Fri, 21 Jun 2024 16:18:57 GMT
ステータス: 処理完了
システム内更新日: 2024-06-24 13:03:22.936927
Title: Interval Analysis in Industrial-Scale BMC Software Verifiers: A Case Study
Title（参考訳）: 産業用BMCソフトウェア検証における区間解析--事例研究
Authors: Rafael Sá Menezes, Edoardo Manino, Fedor Shmarov, Mohannad Aldughaim, Rosiane de Freitas, Lucas C. Cordeiro,
Abstract要約: 我々は,間隔解析の計算コストが,BMCの性能を十分に向上させ,その使用を正当化するか否かを評価する。その結果,203個のベンチマークを解くには区間解析が不可欠であることが示唆された。
参考スコア（独自算出の注目度）: 4.024189528766689
License: http://creativecommons.org/licenses/by/4.0/
Abstract: Bounded Model Checking (BMC) is a widely used software verification technique. Despite its successes, the technique has several limiting factors, from state-space explosion to lack of completeness. Over the years, interval analysis has repeatedly been proposed as a partial solution to these limitations. In this work, we evaluate whether the computational cost of interval analysis yields significant enough improvements in BMC's performance to justify its use. In more detail, we quantify the benefits of interval analysis on two benchmarks: the Intel Core Power Management firmware and 9537 programs in the ReachSafety category of the International Competition on Software Verification. Our results show that interval analysis is essential in solving 203 unique benchmarks.
Abstract（参考訳）: BMC(Bunded Model Checking)は、広く使われているソフトウェア検証手法である。その成功にもかかわらず、この技術には、状態空間の爆発から完全性の欠如まで、いくつかの制限要因がある。長年にわたり、これらの制限に対する部分解として区間解析が何度も提案されてきた。本研究では,時間間隔解析の計算コストがBMCの性能を大幅に向上させ,その使用を正当化するか否かを評価する。より詳しくは、Intel Core Power Managementファームウェアと、International Competition on Software VerificationのReachSafetyカテゴリの9537プログラムの2つのベンチマークでインターバル分析の利点を定量化する。その結果,203個のベンチマークを解くには区間解析が不可欠であることが示唆された。

関連論文リスト

Leveraging Slither and Interval Analysis to build a Static Analysis Tool [0.0]
本稿では,現在最先端の分析ツールで検出されていない,あるいは完全に検出されていない欠陥の発見に向けた進展について述べる。我々は,Slither上に構築された動作ソリューションを開発し,各命令の実行時の契約状態を評価する。
論文参考訳（メタデータ） (2024-10-31T09:28:09Z)
Step-by-Step Reasoning for Math Problems via Twisted Sequential Monte Carlo [55.452453947359736]
Twisted Sequential Monte Carlo(TSMC)に基づく新しい検証手法を提案する。 TSMCを大規模言語モデルに適用し、部分解に対する将来的な報酬を推定する。このアプローチは、ステップワイドなヒューマンアノテーションを必要としない、より直接的なトレーニングターゲットをもたらす。
論文参考訳（メタデータ） (2024-10-02T18:17:54Z)
MR-Ben: A Meta-Reasoning Benchmark for Evaluating System-2 Thinking in LLMs [55.20845457594977]
大規模言語モデル(LLM)は、問題解決と意思決定の能力の向上を示している。本稿ではメタ推論技術を必要とするプロセスベースのベンチマークMR-Benを提案する。メタ推論のパラダイムは,システム2のスロー思考に特に適しています。
論文参考訳（メタデータ） (2024-06-20T03:50:23Z)
ESBMC v7.4: Harnessing the Power of Intervals [4.6232063855710654]
ESBMCはモデルチェックのために多くの最先端技術を実装しています。新しい機能によって、サポート対象のプログラムやプロパティの検証結果が得られます。 ESBMCは、検証性能を向上させるために、プログラム内の式を新しい間隔で解析する。
論文参考訳（メタデータ） (2023-12-22T14:56:46Z)
Formal Runtime Error Detection During Development in the Automotive Industry [0.1611401281366893]
安全関連ソフトウェアでは,音声静的プログラム解析を用いて実行時エラーの欠如を証明することが推奨されている。この分析は、開発者が長時間実行し、多くの誤報を発生させるため、しばしば重荷と見なされる。本稿では,自動推論契約がモジュールレベルの解析にどのようにコンテキストを追加するかを示す。
論文参考訳（メタデータ） (2023-10-25T08:44:52Z)
Timing Analysis of Embedded Software Updates [1.7027593388928293]
組込みソフトウェアの実行時間に対する更新の影響を検証するための差分タイミング解析手法であるRETAを提案する。我々は、産業タイミング分析ツールであるaiTへのRETAの統合に適応し、DELTAと呼ばれるツールで完全な実装を開発する。一方,RETA を DELTA から削除することで,リアルタイム解析ツールとして有効に活用し,解析時間を27% 向上させる。
論文参考訳（メタデータ） (2023-04-27T14:19:15Z)
Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification [3.9403985159394144]
有限状態遷移系の安全性を検証するために形式検証アルゴリズムが考案された。 20年経っても、このアルゴリズムはまだハードウェアモデル検査の最先端にある。私たちの貢献は、この重要な20年前の知識ギャップを、ソフトウェア検証にアルゴリズムを採用することで埋めることです。
論文参考訳（メタデータ） (2022-08-09T21:33:19Z)
Probabilistically Robust Learning: Balancing Average- and Worst-case Performance [105.87195436925722]
我々は、正確で不安定な平均ケースと頑健で保守的な最悪のケースのギャップを埋める、堅牢性確率というフレームワークを提案する。理論的には、このフレームワークはパフォーマンスと最悪のケースと平均ケース学習のサンプル複雑さの間のトレードオフを克服する。
論文参考訳（メタデータ） (2022-02-02T17:01:38Z)
MQBench: Towards Reproducible and Deployable Model Quantization Benchmark [53.12623958951738]
MQBenchは、モデル量子化アルゴリズムの評価、分析、およびデプロイ可能性のベンチマークを行う最初の試みである。我々は、CPU、GPU、ASIC、DSPを含む実世界のデプロイのための複数のプラットフォームを選択し、最先端の量子化アルゴリズムを評価する。包括的な分析を行い、直感的、直感的、あるいは反直感的な洞察を見出す。
論文参考訳（メタデータ） (2021-11-05T23:38:44Z)
Tight Mutual Information Estimation With Contrastive Fenchel-Legendre Optimization [69.07420650261649]
我々はFLOと呼ばれる新しい,シンプルで強力なコントラストMI推定器を提案する。実証的に、我々のFLO推定器は前者の限界を克服し、より効率的に学習する。 FLOの有効性は、広範囲なベンチマークを用いて検証され、実際のMI推定におけるトレードオフも明らかにされる。
論文参考訳（メタデータ） (2021-07-02T15:20:41Z)
Approximation Algorithms for Sparse Principal Component Analysis [57.5357874512594]
主成分分析(PCA)は、機械学習と統計学において広く使われている次元削減手法である。スパース主成分分析(Sparse principal Component Analysis)と呼ばれる,スパース主成分負荷を求める様々な手法が提案されている。本研究では,SPCA問題に対するしきい値の精度,時間,近似アルゴリズムを提案する。
論文参考訳（メタデータ） (2020-06-23T04:25:36Z)

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