論文の概要: ESBMC v7.4: Harnessing the Power of Intervals

• arxiv url: http://arxiv.org/abs/2312.14746v1
• Date: Fri, 22 Dec 2023 14:56:46 GMT
• ステータス: 処理完了
• システム内更新日: 2023-12-25 14:39:58.095057
• Title: ESBMC v7.4: Harnessing the Power of Intervals
• Title（参考訳）: ESBMC v7.4: インターバルのパワーを損なう
• Authors: Rafael Menezes, Mohannad Aldughaim, Bruno Farias, Xianzhiyu Li, Edoardo Manino, Fedor Shmarov, Kunjian Song, Franz Brau{\ss}e, Mikhail R. Gadelha, Norbert Tihanyi, Konstantin Korovin, Lucas C. Cordeiro
• Abstract要約: ESBMCはモデルチェックのために多くの最先端技術を実装しています。 新しい機能によって、サポート対象のプログラムやプロパティの検証結果が得られます。 ESBMCは、検証性能を向上させるために、プログラム内の式を新しい間隔で解析する。
• 参考スコア（独自算出の注目度）: 4.6232063855710654
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: ESBMC implements many state-of-the-art techniques for model checking. We report on new and improved features that allow us to obtain verification results for previously unsupported programs and properties. ESBMC employs a new static interval analysis of expressions in programs to increase verification performance. This includes interval-based reasoning over booleans and integers, forward and backward contractors, and particular optimizations related to singleton intervals because of their ubiquity. Other relevant improvements concern the verification of concurrent programs, as well as several operational models, internal ones, and also those of libraries such as pthread and the C mathematics library. An extended memory safety analysis now allows tracking of memory leaks that are considered still reachable.
• Abstract（参考訳）: ESBMCはモデルチェックのために多くの最先端技術を実装しています。 従来サポートされていたプログラムやプロパティの検証結果を得るために,新たに改良された機能について報告する。 ESBMCは、プログラム内の式を静的に解析し、検証性能を向上させる。 これにはブールと整数の区間に基づく推論、前方と後方の請負業者、そしてそれらのユビキティのためにシングルトン間隔に関する特定の最適化が含まれる。 他の関連する改善は、並列プログラムの検証、およびいくつかの操作モデル、内部モデル、およびpthreadやC数学ライブラリなどのライブラリの検証である。 拡張メモリ安全性解析により、到達可能なメモリリークの追跡が可能になった。

関連論文リスト

• MOLA: Enhancing Industrial Process Monitoring Using Multi-Block Orthogonal Long Short-Term Memory Autoencoder [3.7028696448588487]
  産業プロセスの高精度かつ信頼性の高い故障検出を行うために,MOLA: Multi-block Orthogonal Long short-term memory Autoencoder パラダイムを導入する。 本稿では,プロセス変数を専門的なプロセス知識を活用することで,複数のブロックに分類するマルチブロック監視構造を提案する。 テネシー・イーストマン・プロセスに適用することで,MOLAフレームワークの有効性と有効性を示す。
  論文  参考訳（メタデータ） (2024-10-10T00:49:43Z)
• OCTrack: Benchmarking the Open-Corpus Multi-Object Tracking [63.53176412315835]
  オープンコーパス多対象追跡(OCMOT)の新たな実用的課題について検討する。 我々は,OCMOT問題に対する標準評価プラットフォームを提供するために,大規模かつ包括的なベンチマークであるOCTrackBを構築した。
  論文  参考訳（メタデータ） (2024-07-19T05:58:01Z)
• Interval Analysis in Industrial-Scale BMC Software Verifiers: A Case Study [4.024189528766689]
  我々は,間隔解析の計算コストが,BMCの性能を十分に向上させ,その使用を正当化するか否かを評価する。 その結果,203個のベンチマークを解くには区間解析が不可欠であることが示唆された。
  論文  参考訳（メタデータ） (2024-06-21T16:18:57Z)
• Temporally Consistent Referring Video Object Segmentation with Hybrid Memory [98.80249255577304]
  本稿では,参照セグメンテーションとともに時間的一貫性を明示的にモデル化する,エンドツーエンドなR-VOSパラダイムを提案する。 自動生成された高品質の参照マスクを有するフレームの特徴は、残りのフレームをセグメント化するために伝播される。 大規模な実験により,本手法は時間的整合性を著しく向上させることが示された。
  論文  参考訳（メタデータ） (2024-03-28T13:32:49Z)
• Multi-grained Temporal Prototype Learning for Few-shot Video Object Segmentation [156.4142424784322]
  FSVOS(Few-Shot Video Object)は、いくつかのアノテーション付きサポートイメージで定義されるのと同じカテゴリで、クエリビデオ内のオブジェクトをセグメントすることを目的としている。 本稿では,ビデオデータの時間的相関性を扱うために,多粒度時間的ガイダンス情報を活用することを提案する。 提案するビデオIPMTモデルは,2つのベンチマークデータセットにおいて,従来のモデルよりも大幅に優れていた。
  論文  参考訳（メタデータ） (2023-09-20T09:16:34Z)
• Joint Modeling of Feature, Correspondence, and a Compressed Memory for Video Object Segmentation [52.11279360934703]
  現在のビデオオブジェクト(VOS)メソッドは通常、特徴抽出後のカレントフレームと参照フレームの密マッチングを実行する。 本稿では,特徴量,対応性,圧縮メモリの3要素を共同モデリングするための統合VOSフレームワークであるJointFormerを提案する。
  論文  参考訳（メタデータ） (2023-08-25T17:30:08Z)
• A New Era in Software Security: Towards Self-Healing Software via Large Language Models and Formal Verification [8.733354577147093]
  本稿では,Large Language Models(LLM)とFormal Verification戦略を組み合わせたソフトウェア脆弱性の自動修復手法を提案する。 我々は、ESBMC-AIフレームワークを概念実証として、よく認識され、業界に受け入れられたSMTベースのコンテキスト境界モデルチェッカー(ESBMC)と事前訓練されたトランスフォーマーモデルを活用する。 本研究は,バッファオーバーフローや演算オーバーフロー,ポインタ参照障害などの問題を高精度に検出および修正するESBMC-AIの機能を示すものである。
  論文  参考訳（メタデータ） (2023-05-24T05:54:10Z)
• Joint Feature Learning and Relation Modeling for Tracking: A One-Stream Framework [76.70603443624012]
  特徴学習と関係モデリングを統合した新しい一ストリーム追跡(OSTrack)フレームワークを提案する。 このようにして、相互誘導により識別的目標指向特徴を動的に抽出することができる。 OSTrackは、複数のベンチマークで最先端のパフォーマンスを実現しており、特に、ワンショットトラッキングベンチマークのGOT-10kでは印象的な結果を示している。
  論文  参考訳（メタデータ） (2022-03-22T18:37:11Z)
• Algorithm to Compilation Co-design: An Integrated View of Neural Network Sparsity [0.8566457170664925]
  BERT言語モデルの変圧器ブロックの重み付けに構造化および非構造化プルーニングを適用した。 本研究では,モデル決定と空間的拡張実行に対する直接的影響の関係について検討する。
  論文  参考訳（メタデータ） (2021-06-16T15:13:26Z)
• Online Multiple Object Tracking with Cross-Task Synergy [120.70085565030628]
  位置予測と埋め込み結合の相乗効果を考慮した新しい統一モデルを提案する。 この2つのタスクは、時間認識対象の注意と注意の注意、およびアイデンティティ認識メモリ集約モデルによってリンクされる。
  論文  参考訳（メタデータ） (2021-04-01T10:19:40Z)
• GRAPHSPY: Fused Program Semantic-Level Embedding via Graph Neural Networks for Dead Store Detection [4.82596017481926]
  低オーバーヘッドで不必要なメモリ操作をインテリジェントに識別するための学習精度の高いアプローチを提案する。 プログラムセマンティクスの抽出にいくつかの有意なグラフニューラルネットワークモデルを適用することにより,新しいハイブリッドなプログラム埋め込み手法を提案する。 その結果、我々のモデルは精度の90%を達成でき、最先端ツールのオーバーヘッドの半分程度しか発生しないことがわかった。
  論文  参考訳（メタデータ） (2020-11-18T19:17:15Z)

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

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