論文の概要: 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を目標とし、検証ツールのエントリー障壁を低くし、自動化を改善して証明効率を向上させるとともに、プログラムとその検証結果のより深い理解を促進する。

関連論文リスト

• 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)
• FACTS&EVIDENCE: An Interactive Tool for Transparent Fine-Grained Factual Verification of Machine-Generated Text [39.804889153032526]
  Facts&Evidenceは、複雑なテキストのユーザ主導検証のためのインタラクティブツールである。 個々の主張の信頼性を可視化し、モデル決定と複数の多様な証拠ソースへの帰属を説明する。
  論文  参考訳（メタデータ） (2025-03-19T00:14:55Z)
• 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)

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

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