論文の概要: Non-Termination Proving: 100 Million LoC and Beyond

• arxiv url: http://arxiv.org/abs/2509.05293v1
• Date: Fri, 05 Sep 2025 17:58:45 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-09-08 14:27:25.680639
• Title: Non-Termination Proving: 100 Million LoC and Beyond
• Title（参考訳）: 非ターミネーション証明:1億LOC以上
• Authors: Julien Vanegue, Jules Villard, Peter O'Hearn, Azalea Raad,
• Abstract要約: 我々は,大規模プログラムにおける非終端(発散)を示すための証明手法であるPulse Infiniteについて報告する。 Pulse InfiniteをC、C++、Hackで書かれた1億行以上のオープンソースおよびプロプライエタリなソフトウェアに適用します。
• 参考スコア（独自算出の注目度）: 0.48998185508205744
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We report on our tool, Pulse Infinite, that uses proof techniques to show non-termination (divergence) in large programs. Pulse Infinite works compositionally and under-approximately: the former supports scale, and the latter ensures soundness for proving divergence. Prior work focused on small benchmarks in the tens or hundreds of lines of code (LoC), and scale limits their practicality: a single company may have tens of millions, or even hundreds of millions of LoC or more. We report on applying Pulse Infinite to over a hundred million lines of open-source and proprietary software written in C, C++, and Hack, identifying over 30 previously unknown issues, establishing a new state of the art for detecting divergence in real-world codebases.
• Abstract（参考訳）: 我々は,大規模プログラムにおける非終端(発散)を示すための証明手法であるPulse Infiniteについて報告する。 前者はスケールをサポートし、後者は分岐を証明するための音性を保証する。 以前の作業では、数千行ないし数百行のコード(LoC)の小さなベンチマークに重点を置いていた。 我々は、C、C++、Hackで書かれた1億行以上のオープンソースおよびプロプライエタリなソフトウェアにPulse Infiniteを適用し、30以上の既知の問題を識別し、現実世界のコードベースにおける分岐を検出するための新しい最先端技術を確立することを報告した。

関連論文リスト

• Is Compression Really Linear with Code Intelligence? [60.123628177110206]
  textitFormat Annealingは、事前訓練されたモデルの本質的な能力を同等に評価するために設計された、軽量で透明なトレーニング手法である。 我々の経験的結果は、測定されたコードインテリジェンスとビット・パー・キャラクタ(BPC)の基本的な対数関係を明らかにする。 私たちの研究は、コードインテリジェンスの開発における圧縮の役割をより微妙に理解し、コードドメインにおける堅牢な評価フレームワークに貢献します。
  論文  参考訳（メタデータ） (2025-05-16T16:59:14Z)
• Identifying Bug Inducing Commits by Combining Fault Localisation and Code Change Histories [10.027862394831669]
  BIC(Bug Inducing Commit)は、コミットにバグを導入するコード変更である。 我々は、最近修正されたコード要素がある場合、コミットがBICになる可能性が高いというコア概念でBICを識別することを目的としたFonteと呼ばれるテクニックを提案する。 フォンテは最先端のBIC識別技術を大きく上回り、最大45.8%のMRRを達成している。
  論文  参考訳（メタデータ） (2025-02-18T15:02:22Z)
• Black-Box Adversarial Attacks on LLM-Based Code Completion [5.633172380505533]
  本研究では,最先端のブラックボックスLCMベースのコード補完エンジンが敵にひそかに偏っていることを実証する。 私たちはこの目標を達成する最初の攻撃、INSECを紹介します。 さまざまな最先端のオープンソースモデルやブラックボックスの商用サービスで評価することで、INSECの幅広い適用性と有効性を実証する。
  論文  参考訳（メタデータ） (2024-08-05T14:31:26Z)
• Theoretically Achieving Continuous Representation of Oriented Bounding Boxes [64.15627958879053]
  本論文は,オブジェクト指向境界ボックス表現における不連続性を完全に解決しようとする試みである。 本研究では,既存の検出器に容易に統合可能なCOBB(Continuous OBB)という新しい表現法を提案する。 OOD評価のためのオープンソースのディープラーニングフレームワークJittorの検出ツールボックスJDetをベースとした,モジュール化されたベンチマークを開発した。
  論文  参考訳（メタデータ） (2024-02-29T09:27:40Z)
• DeepSeek-Coder: When the Large Language Model Meets Programming -- The Rise of Code Intelligence [42.517055368627226]
  私たちはDeepSeek-Coderシリーズを紹介します。これは、サイズが1.3Bから33Bまでのオープンソースのコードモデルで、2兆トークンでゼロからトレーニングされています。 評価の結果、DeepSeek-Coderは複数のベンチマークでオープンソースのコードモデル間で最先端のパフォーマンスを実現していることがわかった。 DeepSeek-Coderモデルは、調査と制限なしの商用使用の両方を可能にする寛容なライセンス下にある。
  論文  参考訳（メタデータ） (2024-01-25T14:17:53Z)
• EndWatch: A Practical Method for Detecting Non-Termination in Real-World Software [30.67959999716073]
  本研究では,テストによる無限ループによる非終端検出のための,EndWatchと呼ばれる実用的終端チェック手法を提案する。 我々は、状態の再確認に基づいて、非終端オラクルを生成する2つの方法を紹介した。 非終端オラクルは、大規模なプログラムで非終端を検出するテストツールに組み込むことができる。
  論文  参考訳（メタデータ） (2023-12-06T08:13:30Z)
• Fault-Tolerant Computing with Single Qudit Encoding [49.89725935672549]
  単一マルチレベルキューディットに実装された安定化器量子エラー訂正符号について論じる。 これらのコードは、quditの特定の物理的エラーに合わせてカスタマイズすることができ、効果的にそれらを抑制することができる。 分子スピン四重項上のフォールトトレラントな実装を実証し、線形キューディットサイズのみの成長を伴うほぼ指数関数的な誤差抑制を示す。
  論文  参考訳（メタデータ） (2023-07-20T10:51:23Z)

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

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