論文の概要: Checkification: A Practical Approach for Testing Static Analysis Truths

• arxiv url: http://arxiv.org/abs/2501.12093v1
• Date: Tue, 21 Jan 2025 12:38:04 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-01-22 14:23:29.746223
• Title: Checkification: A Practical Approach for Testing Static Analysis Truths
• Title（参考訳）: 検証:静的解析の真実をテストするための実践的アプローチ
• Authors: Daniela Ferreiro, Ignacio Casso, Jose F. Morales, Pedro López-García, Manuel V. Hermenegildo,
• Abstract要約: 本稿では,抽象解釈に基づく静的アナライザの試験法を提案する。 このアプローチの主な利点は、Ciaoアサーションベースのバリデーションフレームワーク内で直接フレーミングすることによる、シンプルさにあります。 我々は、CiaoPP静的解析器にアプローチを適用し、合理的なオーバーヘッドを伴う多くのバグを特定した。
• 参考スコア（独自算出の注目度）: 0.0
• License:
• Abstract: Static analysis is an essential component of many modern software development tools. Unfortunately, the ever-increasing complexity of static analyzers makes their coding error-prone. Even analysis tools based on rigorous mathematical techniques, such as abstract interpretation, are not immune to bugs. Ensuring the correctness and reliability of software analyzers is critical if they are to be inserted in production compilers and development environments. While compiler validation has seen notable success, formal validation of static analysis tools remains relatively unexplored. In this paper, we propose a method for testing abstract interpretation-based static analyzers. Broadly, it consists in checking, over a suite of benchmarks, that the properties inferred statically are satisfied dynamically. The main advantage of our approach lies in its simplicity, which stems directly from framing it within the Ciao assertion-based validation framework, and its blended static/dynamic assertion checking approach. We demonstrate that in this setting, the analysis can be tested with little effort by combining the following components already present in the framework: 1) the static analyzer, which outputs its results as the original program source with assertions interspersed; 2) the assertion run-time checking mechanism, which instruments a program to ensure that no assertion is violated at run time; 3) the random test case generator, which generates random test cases satisfying the properties present in assertion preconditions; and 4) the unit-test framework, which executes those test cases. We have applied our approach to the CiaoPP static analyzer, resulting in the identification of many bugs with reasonable overhead. Most of these bugs have been either fixed or confirmed, helping us detect a range of errors not only related to analysis soundness but also within other aspects of the framework.
• Abstract（参考訳）: 静的解析は多くの現代のソフトウェア開発ツールの重要なコンポーネントである。 残念なことに、静的アナライザの複雑さが増しているため、コーディングエラーが発生します。 抽象解釈のような厳密な数学的手法に基づく分析ツールでさえ、バグに免疫がない。 ソフトウェアアナライザの正しさと信頼性の確保は、製品コンパイラや開発環境に挿入する上で重要である。 コンパイラのバリデーションは目覚ましい成功を収めているが、静的解析ツールの形式的バリデーションはいまだに探索されていない。 本稿では,抽象解釈に基づく静的解析器の試験法を提案する。 広くは、一連のベンチマークで、静的に推論されたプロパティが動的に満足していることをチェックすることで構成される。 このアプローチの主な利点は、Ciaoアサーションベースのバリデーションフレームワーク内で直接フレーミングすることによる、単純さと、そのブレンドされた静的/動的アサーションチェックアプローチにあります。 この環境では、フレームワークにすでに存在する以下のコンポーネントを組み合わせることで、分析をほとんど努力せずにテストできることを実証します。 1) アサーションが分散した元のプログラムソースとして結果を出力する静的解析器 2) アサーション実行時チェック機構は,実行時にアサーションが違反しないことを保証するプログラムを実行する。 3) アサーション前条件で存在する特性を満たすランダムなテストケースを生成するランダムなテストケースジェネレータ 4) これらのテストケースを実行するユニットテストフレームワーク。 我々は、CiaoPP静的解析器にアプローチを適用し、合理的なオーバーヘッドを伴う多くのバグを特定した。 これらのバグのほとんどは、修正または確認されているため、分析の健全性だけでなく、フレームワークの他の側面においても、さまざまなエラーを検出するのに役立ちます。

関連論文リスト

• Scaling Symbolic Execution to Large Software Systems [0.0]
  シンボル実行は、プログラム検証とバグ検出ソフトウェアの両方で使用される一般的な静的解析手法である。 我々は、Clang Static Analyzerと呼ばれるエラー検出フレームワークと、その周辺に構築されたインフラストラクチャーであるCodeCheckerに焦点を当てた。
  論文  参考訳（メタデータ） (2024-08-04T02:54:58Z)
• Customizing Static Analysis using Codesearch [1.7205106391379021]
  様々な静的解析アプリケーションを記述するのによく使われる言語は、Datalogである。 アプリケーションセキュリティと静的分析の専門家のための慣れ親しんだフレームワークを提供すると同時に、開発者がカスタムの静的解析ツールを簡単に構築できるようにすることを目標としています。 我々のアプローチでは,高速ランタイムを持つプログラムのみを含むDatalogの亜種であるStarLangという言語を導入しています。
  論文  参考訳（メタデータ） (2024-04-19T09:50:02Z)
• Supporting Error Chains in Static Analysis for Precise Evaluation Results and Enhanced Usability [2.8557828838739527]
  静的解析は、固定位置よりも脆弱性が現れる場所を報告する傾向にある。 これは仮定された偽陽性や不正確な結果を引き起こす可能性がある。 我々は、既存の静的解析アルゴリズムを適応させ、マニフェストと固定位置を区別できるように設計した。
  論文  参考訳（メタデータ） (2024-03-12T16:46:29Z)
• Understanding and Detecting Annotation-Induced Faults of Static Analyzers [4.824956210843882]
  本稿では,注釈誘発断層(AIF)の総合的研究について紹介する。 PMD、SpotBugs、CheckStyle、Infer、SonarQube、Sootの6つのオープンソースおよび人気のある静的アナライザの246の問題を解析した。
  論文  参考訳（メタデータ） (2024-02-22T08:09:01Z)
• From Static Benchmarks to Adaptive Testing: Psychometrics in AI Evaluation [60.14902811624433]
  本稿では,静的評価手法から適応テストへのパラダイムシフトについて論じる。 これには、ベンチマークで各テスト項目の特性と価値を推定し、リアルタイムでアイテムを動的に調整することが含まれる。 我々は、AI評価にサイコメトリックを採用する現在のアプローチ、アドバンテージ、そして根底にある理由を分析します。
  論文  参考訳（メタデータ） (2023-06-18T09:54:33Z)
• A Static Evaluation of Code Completion by Large Language Models [65.18008807383816]
  単純なプログラミング問題に対するモデル生成コードの機能的正当性を評価するために,実行ベースベンチマークが提案されている。 プログラムを実行せずにエラーを検出するlinterのような静的解析ツールは、コード生成モデルを評価するために十分に研究されていない。 抽象構文木を利用して,Pythonのコード補完における静的エラーを定量化する静的評価フレームワークを提案する。
  論文  参考訳（メタデータ） (2023-06-05T19:23:34Z)
• Learning to Reduce False Positives in Analytic Bug Detectors [12.733531603080674]
  偽陽性のバグ警告を識別するためのトランスフォーマーに基づく学習手法を提案する。 我々は,静的解析の精度を17.5%向上させることができることを示した。
  論文  参考訳（メタデータ） (2022-03-08T04:26:26Z)
• D2A: A Dataset Built for AI-Based Vulnerability Detection Methods Using Differential Analysis [55.15995704119158]
  静的解析ツールによって報告されたラベル問題に対する差分解析に基づくアプローチであるD2Aを提案する。 D2Aを使用して大きなラベル付きデータセットを生成し、脆弱性識別のためのモデルをトレーニングします。
  論文  参考訳（メタデータ） (2021-02-16T07:46:53Z)
• Beyond Accuracy: Behavioral Testing of NLP models with CheckList [66.42971817954806]
  CheckList は NLP モデルをテストするためのタスクに依存しない方法論である。 CheckListには、包括的なテストのアイデアを促進する一般的な言語機能とテストタイプのマトリックスが含まれている。 ユーザスタディでは、CheckListのNLP実践者が2倍の数のテストを作成し、それのないユーザの約3倍のバグを発見しました。
  論文  参考訳（メタデータ） (2020-05-08T15:48:31Z)
• The Curse of Performance Instability in Analysis Datasets: Consequences, Source, and Suggestions [93.62888099134028]
  自然言語推論(NLI)および読み込み(RC)解析/ストレスセットにおける最先端モデルの性能は極めて不安定であることがわかった。 このことは、(1)不安定さがこれらの分析セットに基づいて引き出された結論の信頼性にどのように影響するかという3つの疑問を提起する。 不安定の原因に関する理論的説明と実証的証拠の両方を提示する。
  論文  参考訳（メタデータ） (2020-04-28T15:41:12Z)
• Certified Robustness to Label-Flipping Attacks via Randomized Smoothing [105.91827623768724]
  機械学習アルゴリズムは、データ中毒攻撃の影響を受けやすい。 任意の関数に対するランダム化スムージングの統一的なビューを示す。 本稿では,一般的なデータ中毒攻撃に対して,ポイントワイズで確実に堅牢な分類器を構築するための新しい戦略を提案する。
  論文  参考訳（メタデータ） (2020-02-07T21:28:30Z)

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

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