論文の概要: NEAT: QCP: A Practical Separation Logic-based C Program Verification Tool

• arxiv url: http://arxiv.org/abs/2505.12878v1
• Date: Mon, 19 May 2025 09:04:34 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-05-20 14:57:11.503197
• Title: NEAT: QCP: A Practical Separation Logic-based C Program Verification Tool
• Title（参考訳）: NEAT: QCP: 論理ベースのCプログラム検証ツール
• Authors: Xiwei Wu, Yueyang Feng, Xiaoyang Lu, Tianchuan Lin, Kan Liu, Zhiyi Wang, Shushu Wu, Lihan Xie, Chengxi Yang, Hongyi Zhong, Naijun Zhan, Zhenjiang Hu, Qinxiang Cao,
• Abstract要約: 本稿では,textbf C Programming Verifier (QCP) と呼ばれる新しい検証ツールを紹介する。 QCPは、ユーザインタラクションを強化するために、アサーション言語の洗練されたフロントエンド%シンタクスを組み込んでいる。
• 参考スコア（独自算出の注目度）: 4.449417653464987
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: As software systems increase in size and complexity dramatically, ensuring their correctness, security, and reliability becomes an increasingly formidable challenge. Despite significant advancements in verification techniques and tools, there still remain %these tools still continue to encounter substantial difficulties when applying these tools to complex, real-world scenarios. To address these difficulties, this paper introduces a novel verification tool, called \textbf{Qualified C Programming Verifier (QCP)}. QCP incorporates a refined front-end %syntax of assertion language to enhance user interaction. The proposed assertion language aims to %syntax is designed to lower the entry barrier for verification tools, improve proof efficiency by improving automation, and facilitate a deeper understanding of both the program and its verification results.
• Abstract（参考訳）: ソフトウェアシステムのサイズと複雑さが劇的に増大するにつれて、その正確性、セキュリティ、信頼性がますます深刻な課題になりつつある。 検証技術やツールの大幅な進歩にもかかわらず、これらのツールを複雑で現実的なシナリオに適用する際にも、まだ1%のツールが重大な困難に直面している。 このような問題に対処するため,本稿では,新しい検証ツールである「textbf{Qualified C Programming Verifier (QCP)」を紹介する。 QCPは、ユーザインタラクションを強化するために、アサーション言語の洗練されたフロントエンド%シンタクスを組み込んでいる。 提案するアサーション言語は、%syntaxを目標とし、検証ツールのエントリー障壁を低くし、自動化を改善して証明効率を向上させるとともに、プログラムとその検証結果のより深い理解を促進する。

関連論文リスト

• Position Paper: Programming Language Techniques for Bridging LLM Code Generation Semantic Gaps [3.61356888205659]
  本稿では,大規模言語モデルにおける意味的ギャップを埋めるのに,プログラミング手法の原則的統合が不可欠であることを論じる。 PL技術は、LLM生成コードを統計的パターンマッチングから真に信頼性と信頼性の高いレベルまで高めることができる。
  論文  参考訳（メタデータ） (2025-07-12T04:32:15Z)
• What Challenges Do Developers Face When Using Verification-Aware Programming Languages? [45.44831696628473]
  ソフトウェア開発では、ソフトウェア信頼性の増大はテストを伴うことが多い。 複雑でクリティカルなシステムでは、開発者はDesign by Contract(DbC)メソッドを使って、ソフトウェアコンポーネントが満たさなければならない正確な仕様を定義することができます。 VA(Verification-Aware)プログラミング言語は、DbCとコンパイル時または実行時の形式的検証をサポートし、従来のテストよりも正確性を保証する。
  論文  参考訳（メタデータ） (2025-06-30T10:17:39Z)
• Enhancing Tool Learning in Large Language Models with Hierarchical Error Checklists [49.450160442348825]
  本稿では,階層型ツールエラーチェックリスト(HiTEC)フレームワークを提案する。 HiTECでは、共通、クロスツールの問題を特定するグローバルエラーチェックリストと、ツール固有の、コンテキストの障害をターゲットとするローカルエラーチェックリストという、2段階のアプローチを導入している。 本フレームワークは,基本手法と比較してパラメータ充足精度とツールコール成功率を大幅に改善する。
  論文  参考訳（メタデータ） (2025-05-28T08:39:35Z)
• Enhancing Large Language Models with Faster Code Preprocessing for Vulnerability Detection [0.0]
  既存のSCoPEフレームワーク上に構築し、パフォーマンスを改善した拡張バージョンであるSCoPE2を導入します。 SCoPE2による処理時間を97.3%削減し,脆弱性検出のためのLarge Language Model(LLM)のF1スコアを改良した。
  論文  参考訳（メタデータ） (2025-05-08T19:00:11Z)
• Acting Less is Reasoning More! Teaching Model to Act Efficiently [87.28134636548705]
  ツール統合推論は、タスクを解決するために外部ツールを呼び出す機能によって、大きな言語モデルを拡張します。 現在のアプローチは、外部ツールの使用効率や必要性を考慮せずに、最終的な正確性のためにのみ最適化されている。 最小限のツールコールで正確な回答をモデルに提示するフレームワークを提案する。 このアプローチでは,ツールコールを最大68.3%削減し,ツールの生産性を最大215.4%向上すると同時に,同等の回答精度を維持している。
  論文  参考訳（メタデータ） (2025-04-21T05:40:05Z)
• FACTS&EVIDENCE: An Interactive Tool for Transparent Fine-Grained Factual Verification of Machine-Generated Text [39.804889153032526]
  Facts&Evidenceは、複雑なテキストのユーザ主導検証のためのインタラクティブツールである。 個々の主張の信頼性を可視化し、モデル決定と複数の多様な証拠ソースへの帰属を説明する。
  論文  参考訳（メタデータ） (2025-03-19T00:14:55Z)
• Adaptive Tool Use in Large Language Models with Meta-Cognition Trigger [49.81945268343162]
  我々は,外部ツール利用のための適応型意思決定戦略であるMeCoを提案する。 MeCoは、表現空間内の高レベル認知信号をキャプチャすることで、メタ認知スコアを定量化する。 MeCoは微調整不要で、最小限のコストがかかる。
  論文  参考訳（メタデータ） (2025-02-18T15:45:01Z)
• ToolCoder: A Systematic Code-Empowered Tool Learning Framework for Large Language Models [49.04652315815501]
  ツール学習は、大規模な言語モデル(LLM)にとって、外部ツールとのインタラクションを通じて、複雑な現実世界のタスクを解決する重要な機能として登場した。 本稿では,ツール学習をコード生成タスクとして再編成する新しいフレームワークであるToolCoderを提案する。
  論文  参考訳（メタデータ） (2025-02-17T03:42:28Z)
• Evaluating Pre-Trained Models for Multi-Language Vulnerability Patching [3.220818227251765]
  本稿では,事前学習型言語モデルであるCodeBERTとCodeT5の脆弱性パッチ自動適用の可能性について検討する。 これらのモデルの精度、計算効率、脆弱性のあるコードパッチの長さがパフォーマンスに与える影響について評価する。
  論文  参考訳（メタデータ） (2025-01-13T13:51:05Z)
• Development and Adoption of SATD Detection Tools: A State-of-practice Report [5.670597842524448]
  Self-Admitted Technical Debt (SATD)は、開発者が故意に最適化されたソリューションをコードに導入するインスタンスを指す。 本稿では,SATD検出ツールの開発と導入に関する総合的な状況報告を提供する。
  論文  参考訳（メタデータ） (2024-12-18T12:06:53Z)
• Improving LLM Reasoning through Scaling Inference Computation with Collaborative Verification [52.095460362197336]
  大規模言語モデル(LLM)は一貫性と正確な推論に苦しむ。 LLMは、主に正しいソリューションに基づいて訓練され、エラーを検出して学習する能力を減らす。 本稿では,CoT(Chain-of-Thought)とPoT(Program-of-Thought)を組み合わせた新しい協調手法を提案する。
  論文  参考訳（メタデータ） (2024-10-05T05:21:48Z)
• Agent-Driven Automatic Software Improvement [55.2480439325792]
  本提案は,Large Language Models (LLMs) を利用したエージェントの展開に着目して,革新的なソリューションの探求を目的とする。 継続的学習と適応を可能にするエージェントの反復的性質は、コード生成における一般的な課題を克服するのに役立ちます。 我々は,これらのシステムにおける反復的なフィードバックを用いて,エージェントの基盤となるLLMをさらに微調整し,自動化されたソフトウェア改善のタスクに整合性を持たせることを目指している。
  論文  参考訳（メタデータ） (2024-06-24T15:45:22Z)
• Lemur: Integrating Large Language Models in Automated Program Verification [10.221822902660458]
  自動プログラム検証のためのLLMと自動推論器のパワーを組み合わせるための一般的な手法を提案する。 本稿では,音声自動検証手法として計算をインスタンス化し,一連の合成および競合ベンチマークの実践的改善を実証する。
  論文  参考訳（メタデータ） (2023-10-07T16:44:53Z)
• Guess & Sketch: Language Model Guided Transpilation [59.02147255276078]
  学習されたトランスパイレーションは、手作業による書き直しやエンジニアリングの取り組みに代わるものだ。 確率的ニューラルネットワークモデル(LM)は、入力毎に可塑性出力を生成するが、正確性を保証するコストがかかる。 Guess & Sketch は LM の特徴からアライメントと信頼性情報を抽出し、意味的等価性を解決するためにシンボリック・ソルバに渡す。
  論文  参考訳（メタデータ） (2023-09-25T15:42:18Z)
• FacTool: Factuality Detection in Generative AI -- A Tool Augmented Framework for Multi-Task and Multi-Domain Scenarios [87.12753459582116]
  より広い範囲のタスクは、生成モデルによって処理されると、事実エラーを含むリスクが増大する。 大規模言語モデルにより生成されたテキストの事実誤りを検出するためのタスクおよびドメインに依存しないフレームワークであるFacToolを提案する。
  論文  参考訳（メタデータ） (2023-07-25T14:20:51Z)

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

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