Fugu-MT 論文翻訳(概要): Scaling Symbolic Execution to Large Software Systems

論文の概要: Scaling Symbolic Execution to Large Software Systems

arxiv url: http://arxiv.org/abs/2408.01909v1
Date: Sun, 4 Aug 2024 02:54:58 GMT
ステータス: 処理完了
システム内更新日: 2024-08-06 17:51:14.491783
Title: Scaling Symbolic Execution to Large Software Systems
Title（参考訳）: 大規模ソフトウェアシステムへのシンボリックな実行のスケーリング
Authors: Gabor Horvath, Reka Kovacs, Zoltan Porkolab,
Abstract要約: シンボル実行は、プログラム検証とバグ検出ソフトウェアの両方で使用される一般的な静的解析手法である。我々は、Clang Static Analyzerと呼ばれるエラー検出フレームワークと、その周辺に構築されたインフラストラクチャーであるCodeCheckerに焦点を当てた。
参考スコア（独自算出の注目度）: 0.0
License: http://creativecommons.org/licenses/by/4.0/
Abstract: Static analysis is the analysis of a program without executing it, usually carried out by an automated tool. Symbolic execution is a popular static analysis technique used both in program verification and in bug detection software. It works by interpreting the code, introducing a symbol for each value unknown at compile time (e.g. user-given inputs), and carrying out calculations symbolically. The analysis engine strives to explore multiple execution paths simultaneously, although checking all paths is an intractable problem, due to the vast number of possibilities. We focus on an error finding framework called the Clang Static Analyzer, and the infrastructure built around it named CodeChecker. The emphasis is on achieving end-to-end scalability. This includes the run time and memory consumption of the analysis, bug presentation to the users, automatic false positive suppression, incremental analysis, pattern discovery in the results, and usage in continuous integration loops. We also outline future directions and open problems concerning these tools. While a rich literature exists on program verification software, error finding tools normally need to settle for survey papers on individual techniques. In this paper, we not only discuss individual methods, but also how these decisions interact and reinforce each other, creating a system that is greater than the sum of its parts. Although the Clang Static Analyzer can only handle C-family languages, the techniques introduced in this paper are mostly language-independent and applicable to other similar static analysis tools.
Abstract（参考訳）: 静的解析とは、実行せずにプログラムを解析することであり、通常は自動化ツールによって実行される。シンボル実行は、プログラム検証とバグ検出ソフトウェアの両方で使用される一般的な静的解析手法である。コードを解釈し、コンパイル時に未知の値(例えばユーザ入力)ごとにシンボルを導入し、シンボル的に計算を実行する。分析エンジンは、複数の実行パスを同時に探索するが、多くの可能性のために、すべてのパスをチェックすることは難解な問題である。我々は、Clang Static Analyzerと呼ばれるエラー検出フレームワークと、その周辺に構築されたインフラストラクチャーであるCodeCheckerに焦点を当てた。強調するのは、エンドツーエンドのスケーラビリティの実現だ。これには、分析の実行時間とメモリ消費、ユーザへのバグプレゼンテーション、自動偽陽性の抑制、インクリメンタル分析、結果のパターン発見、継続的インテグレーションループの使用などが含まれる。また、これらのツールに関する今後の方向性と課題についても概説する。プログラム検証ソフトウェアには豊富な文献が存在するが、エラー検出ツールは通常、個々の技術に関する調査論文のために解決する必要がある。本稿では,個別の手法だけでなく,これらの決定がどのように相互に相互作用し,相互に強化するかについても論じる。 Clang Static AnalyzerはCファミリー言語しか扱えないが、本稿で紹介される技術は主に言語に依存しず、他の類似の静的解析ツールに適用できる。

関連論文リスト

Easing Maintenance of Academic Static Analyzers [0.0]
Mopsaは、音を出すことを目的とした静的分析プラットフォームである。この記事では、2017年以来のMopsaのメンテナンスを簡素化するために、私たちが作り出したツールとテクニックについて説明する。
論文参考訳（メタデータ） (2024-07-17T11:29:21Z)
Efficacy of static analysis tools for software defect detection on open-source projects [0.0]
この調査では、SonarQube、PMD、Checkstyle、FindBugsといった一般的な分析ツールを使って比較を行った。その結果,SonarQubeの欠陥検出は,他のツールと比較してかなり優れていることがわかった。
論文参考訳（メタデータ） (2024-05-20T19:05:32Z)
Customizing Static Analysis using Codesearch [1.7205106391379021]
様々な静的解析アプリケーションを記述するのによく使われる言語は、Datalogである。アプリケーションセキュリティと静的分析の専門家のための慣れ親しんだフレームワークを提供すると同時に、開発者がカスタムの静的解析ツールを簡単に構築できるようにすることを目標としています。我々のアプローチでは,高速ランタイムを持つプログラムのみを含むDatalogの亜種であるStarLangという言語を導入しています。
論文参考訳（メタデータ） (2024-04-19T09:50:02Z)
Integrating Static Code Analysis Toolchains [0.8246494848934447]
最先端のツールチェーンは、テスト実行とビルド自動化、テスト、要件、設計情報間のトレーサビリティをサポートする。当社のアプローチでは,これらの機能をすべて組み合わせて,静的コード解析を取り入れて,トレーサビリティをソースコードレベルにまで拡張しています。
論文参考訳（メタデータ） (2024-03-09T18:59:50Z)
Symbol-Specific Sparsification of Interprocedural Distributive Environment Problems [3.9777369380822956]
本稿では,言語間分散環境(IDE)フレームワークに適合する静的解析のスパース化を実現するフレームワークであるSparse IDEを提案する。 SparseHeros上に線形定数伝搬解析クライアントを設計,実装,評価する。
論文参考訳（メタデータ） (2024-01-26T12:31:30Z)
ControlLLM: Augment Language Models with Tools by Searching on Graphs [97.62758830255002]
我々は,大規模言語モデル(LLM)が実世界のタスクを解くためのマルチモーダルツールを利用できる新しいフレームワークであるControlLLMを提案する。フレームワークは,(1)複雑なタスクを明確なサブタスクに分割し,入力と出力を適切に定義したサブタスクに分解するtextittask Decomposer,(2)構築済みのツールグラフ上で最適なソリューションパスを探索する textitThoughts-on-Graph(ToG)パラダイム,(3)ソリューションパスを解釈して実行するリッチなツールボックスを備えた textitexecution Engine,の3つの主要なコンポーネントから構成される。
論文参考訳（メタデータ） (2023-10-26T21:57:21Z)
Guess & Sketch: Language Model Guided Transpilation [59.02147255276078]
学習されたトランスパイレーションは、手作業による書き直しやエンジニアリングの取り組みに代わるものだ。確率的ニューラルネットワークモデル(LM)は、入力毎に可塑性出力を生成するが、正確性を保証するコストがかかる。 Guess & Sketch は LM の特徴からアライメントと信頼性情報を抽出し、意味的等価性を解決するためにシンボリック・ソルバに渡す。
論文参考訳（メタデータ） (2023-09-25T15:42:18Z)
A Static Evaluation of Code Completion by Large Language Models [65.18008807383816]
単純なプログラミング問題に対するモデル生成コードの機能的正当性を評価するために,実行ベースベンチマークが提案されている。プログラムを実行せずにエラーを検出するlinterのような静的解析ツールは、コード生成モデルを評価するために十分に研究されていない。抽象構文木を利用して,Pythonのコード補完における静的エラーを定量化する静的評価フレームワークを提案する。
論文参考訳（メタデータ） (2023-06-05T19:23:34Z)
Structural Analysis of Branch-and-Cut and the Learnability of Gomory Mixed Integer Cuts [88.94020638263467]
ブランチ・アンド・カット(ブランチ・アンド・カット)として知られる分岐・アンド・バウンドアルゴリズムにおける切断平面の組み入れは、現代の整数計画解法のバックボーンを形成する。入力整数プログラムに付加される切断平面を定義するパラメータの変化により、アルゴリズムの各ステップがどのように影響を受けるかをピン留めする、分岐切断の新たな構造解析を行う。この分析の主な応用は、機械学習を用いてブランチ・アンド・カット時にどの切断面を適用するかを決定するためのサンプルの複雑性保証を導出することである。
論文参考訳（メタデータ） (2022-04-15T03:32:40Z)
Searching for More Efficient Dynamic Programs [61.79535031840558]
本稿では,プログラム変換の集合,変換プログラムの効率を評価するための単純な指標,およびこの指標を改善するための探索手順について述べる。実際に、自動検索は初期プログラムの大幅な改善を見出すことができることを示す。
論文参考訳（メタデータ） (2021-09-14T20:52:55Z)
D2A: A Dataset Built for AI-Based Vulnerability Detection Methods Using Differential Analysis [55.15995704119158]
静的解析ツールによって報告されたラベル問題に対する差分解析に基づくアプローチであるD2Aを提案する。 D2Aを使用して大きなラベル付きデータセットを生成し、脆弱性識別のためのモデルをトレーニングします。
論文参考訳（メタデータ） (2021-02-16T07:46:53Z)

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

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