論文の概要: A shallow dive into the depths of non-termination checking for C programs

• arxiv url: http://arxiv.org/abs/2409.12985v1
• Date: Wed, 4 Sep 2024 22:47:46 GMT
• ステータス: 処理完了
• システム内更新日: 2024-11-07 12:25:44.175589
• Title: A shallow dive into the depths of non-termination checking for C programs
• Title（参考訳）: Cプログラムにおける非終端チェックの深さの浅い潜入
• Authors: Ravindra Metta, Hrishikesh Karmarkar, Kumar Madhukar, R Venkatesh, Supratik Chakraborty, Samarjit Chakraborty,
• Abstract要約: Unintended Non-Termination (NT) は、現実世界のソフトウェア開発において一般的である。 実世界のソフトウェアにも有効であるNTチェックのための健全で効率的な手法を提案する。 幅広いソフトウェアベンチマーク実験により、この手法が最先端のNTチェッカーより優れていることが示された。
• 参考スコア（独自算出の注目度）: 3.4144415576897624
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Checking for Non-Termination (NT) of a given program P, i.e., determining if P has at least one non-terminating run, is an undecidable problem that continues to garner significant research attention. While unintended NT is common in real-world software development, even the best-performing tools for NT checking are often ineffective on real-world programs and sometimes incorrect due to unrealistic assumptions such as absence of overflows. To address this, we propose a sound and efficient technique for NT checking that is also effective on realworld software. Given P, we encode the NT property as an assertion inside each loop of P to check for recurrent states in that loop, up to a fixed unwinding depth, using a Bounded Model Checker. The unwinding depth is increased iteratively until either NT is found or a predefined limit is reached. Our experiments on wide ranging software benchmarks show that the technique outperforms state-of-the-art NT checkers
• Abstract（参考訳）: 与えられたプログラムPの非終端チェック(NT)、すなわち、Pが少なくとも1つの非終端ランを持っているかどうかを決定することは、決定不能な問題であり、重要な研究の注目を集め続けている。 非意図のNTは、現実世界のソフトウェア開発では一般的であるが、NTチェックの最高のパフォーマンスツールでさえ、実際のプログラムでは効果がなく、オーバーフローの欠如のような非現実的な仮定のため、しばしば正しくない。 そこで本研究では,実世界のソフトウェアにも有効であるNTチェックのための,健全で効率的な手法を提案する。 P が与えられたとき、我々は NT プロパティを P の各ループ内のアサーションとしてエンコードし、境界モデルチェッカーを用いて、そのループ内のリカレント状態をチェックする。 曲がらない深さは、NTが見つかるか、予め定義された限界に達するまで反復的に増加する。 幅広いソフトウェアベンチマーク実験により、この手法は最先端のNTチェッカーより優れていることが示された。

関連論文リスト

• EndWatch: A Practical Method for Detecting Non-Termination in Real-World Software [30.67959999716073]
  本研究では,テストによる無限ループによる非終端検出のための,EndWatchと呼ばれる実用的終端チェック手法を提案する。 我々は、状態の再確認に基づいて、非終端オラクルを生成する2つの方法を紹介した。 非終端オラクルは、大規模なプログラムで非終端を検出するテストツールに組み込むことができる。
  論文  参考訳（メタデータ） (2023-12-06T08:13:30Z)
• On Pitfalls of Test-Time Adaptation [82.8392232222119]
  TTA(Test-Time Adaptation)は、分散シフトの下で堅牢性に取り組むための有望なアプローチとして登場した。 TTABは,10の最先端アルゴリズム,多種多様な分散シフト,および2つの評価プロトコルを含むテスト時間適応ベンチマークである。
  論文  参考訳（メタデータ） (2023-06-06T09:35:29Z)
• Efficient Deep Reinforcement Learning Requires Regulating Overfitting [91.88004732618381]
  本稿では,高時間差(TD)誤差が深部RLアルゴリズムの性能に悪影響を及ぼす主要な原因であることを示す。 検証TDエラーをターゲットとした簡単なオンラインモデル選択法は,状態ベースDMCおよびGymタスク間で有効であることを示す。
  論文  参考訳（メタデータ） (2023-04-20T17:11:05Z)
• The #DNN-Verification Problem: Counting Unsafe Inputs for Deep Neural Networks [94.63547069706459]
  #DNN-Verification問題は、DNNの入力構成の数を数えることによって安全性に反する結果となる。 違反の正確な数を返す新しい手法を提案する。 安全クリティカルなベンチマークのセットに関する実験結果を示す。
  論文  参考訳（メタデータ） (2023-01-17T18:32:01Z)
• Sound and Complete Verification of Polynomial Networks [55.9260539566555]
  PN(Polynomial Networks)は、最近顔と画像の認識において有望な性能を示した。 分岐とバウンド(BaB)技術に基づくReLUニューラルネットワーク(NN)上の既存の検証アルゴリズムは、PN検証に自明に適用できない。 我々は、VPNと呼ばれるグローバルコンバージェンス保証のためのBaBを備えた新しいバウンダリング手法を考案した。
  論文  参考訳（メタデータ） (2022-09-15T11:50:43Z)
• A Continual Deepfake Detection Benchmark: Dataset, Methods, and Essentials [97.69553832500547]
  本稿では, 既知の生成モデルと未知の生成モデルの両方から, 新たなディープフェイク集合に対する連続的なディープフェイク検出ベンチマーク(CDDB)を提案する。 本研究では,連続的なディープラーニング検出問題に対して,連続的な視覚認識で一般的に使用される多クラス漸進学習手法を適応するために,複数のアプローチを利用する。
  論文  参考訳（メタデータ） (2022-05-11T13:07:19Z)
• Unsupervised Domain Adaptation: A Reality Check [23.79809492395849]
  大規模実験により,UDAアルゴリズムの精度の差が従来考えられていたよりも小さいことを示す。 バリデーションメソッドが任意のUDAトレイン/バルパイプラインの重要なコンポーネントであるという事実にもかかわらず、これは事実です。
  論文  参考訳（メタデータ） (2021-11-30T18:59:04Z)
• CURE: Code-Aware Neural Machine Translation for Automatic Program Repair [11.556110575946631]
  提案するCUREは,3つの新奇性を持つ新しいNMTベースのAPR手法である。 CUREは、APRタスクの前に開発者ライクなソースコードを学ぶために、大きなソフトウェア上でプログラミング言語(PL)モデルを事前にトレーニングします。 第2に、curyは、バギーコードに近いコンパイル可能なパッチとパッチに注目して、より正確な修正を見つける新しいコードアウェア検索戦略をデザインする。
  論文  参考訳（メタデータ） (2021-02-26T22:30:28Z)
• A Lower Bound on DNNF Encodings of Pseudo-Boolean Constraints [3.42658286826597]
  疑似ブール制約をSATにエンコーディングする際の2つの大きな考慮事項は、エンコーディングのサイズとその伝播強度である。 命令されたBDD(OBDD)表現と推論されたCNFエンコーディングがすべて指数的サイズを持つPB制約が存在することが示されている。
  論文  参考訳（メタデータ） (2021-01-06T10:25:22Z)
• Global Optimization of Objective Functions Represented by ReLU Networks [77.55969359556032]
  ニューラルネットワークは複雑で非敵対的な関数を学ぶことができ、安全クリティカルな文脈でそれらの正しい振る舞いを保証することは困難である。 ネットワーク内の障害を見つけるための多くのアプローチ(例えば、敵の例)があるが、これらは障害の欠如を保証できない。 本稿では,最適化プロセスを検証手順に統合し,本手法よりも優れた性能を実現する手法を提案する。
  論文  参考訳（メタデータ） (2020-10-07T08:19:48Z)

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

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