論文の概要: 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数学ライブラリなどのライブラリの検証である。
拡張メモリ安全性解析により、到達可能なメモリリークの追跡が可能になった。
関連論文リスト
- Towards Temporally Consistent Referring Video Object Segmentation [98.80249255577304]
本稿では,参照セグメンテーションとともに時間的一貫性を明示的にモデル化する,エンドツーエンドなR-VOSパラダイムを提案する。
自動生成された高品質の参照マスクを有するフレームの特徴は、残りのフレームをセグメント化するために伝播される。
大規模な実験により,本手法は時間的整合性を著しく向上させることが示された。
論文 参考訳(メタデータ) (2024-03-28T13:32:49Z) - LLVM Static Analysis for Program Characterization and Memory Reuse
Profile Estimation [0.0]
本稿ではLLVMに基づく確率的静的解析手法を提案する。
プログラムの特徴を正確に予測し、プログラムの再利用距離プロファイルを推定する。
その結果,LLVMベースの動的コード解析ツールであるByflと比較して,アプリケーションの特性を正確に予測できることがわかった。
論文 参考訳(メタデータ) (2023-11-20T23:05:06Z) - 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) - Cheaply Evaluating Inference Efficiency Metrics for Autoregressive
Transformer APIs [66.30706841821123]
大規模言語モデル(LLM)は、自然言語処理において多くの最先端システムに電力を供給する。
LLMは、推論時でさえ非常に計算コストが高い。
モデル間での推論効率を比較するための新しい指標を提案する。
論文 参考訳(メタデータ) (2023-05-03T21:51:42Z) - Timing Analysis of Embedded Software Updates [1.7027593388928293]
組込みソフトウェアの実行時間に対する更新の影響を検証するための差分タイミング解析手法であるRETAを提案する。
我々は、産業タイミング分析ツールであるaiTへのRETAの統合に適応し、DELTAと呼ばれるツールで完全な実装を開発する。
一方,RETA を DELTA から削除することで,リアルタイム解析ツールとして有効に活用し,解析時間を27% 向上させる。
論文 参考訳(メタデータ) (2023-04-27T14:19:15Z) - Joint Feature Learning and Relation Modeling for Tracking: A One-Stream
Framework [76.70603443624012]
特徴学習と関係モデリングを統合した新しい一ストリーム追跡(OSTrack)フレームワークを提案する。
このようにして、相互誘導により識別的目標指向特徴を動的に抽出することができる。
OSTrackは、複数のベンチマークで最先端のパフォーマンスを実現しており、特に、ワンショットトラッキングベンチマークのGOT-10kでは印象的な結果を示している。
論文 参考訳(メタデータ) (2022-03-22T18:37:11Z) - GEMEL: Model Merging for Memory-Efficient, Real-Time Video Analytics at
the Edge [10.276140547573437]
エッジビジョンモデル間のアーキテクチャ的類似性を利用した新しいメモリ管理手法であるモデルマージを提案する。
多様なワークロードに対する実験により、GEMELはメモリ使用量を最大60.7%削減し、時間/空間の共有のみと比較して、全体的な精度を8~39%向上することが明らかになった。
論文 参考訳(メタデータ) (2022-01-19T16:45:04Z) - 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)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト(すべての情報・翻訳含む)の品質を保証せず、本サイト(すべての情報・翻訳含む)を使用して発生したあらゆる結果について一切の責任を負いません。