論文の概要: C Analyzer : A Static Program Analysis Tool for C Programs

• arxiv url: http://arxiv.org/abs/2403.12973v1
• Date: Sun, 28 Jan 2024 11:43:16 GMT
• ステータス: 処理完了
• システム内更新日: 2024-03-25 07:27:10.272547
• Title: C Analyzer : A Static Program Analysis Tool for C Programs
• Title（参考訳）: C Analyzer : Cプログラムのための静的プログラム解析ツール
• Authors: Rajendra Kumar Solanki,
• Abstract要約: C Analyzerは、Cプログラムの静的解析のために開発されたツールである。 本研究は,Cプログラムの静的解析に抽象解釈技術を活用することを目的とする。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: In our times, when the world is increasingly becoming more dependent on software programs, writing bug-free, correct programs is crucial. Program verification based on formal methods can guarantee this by detecting run-time errors in safety-critical systems to avoid possible adverse impacts on human life and save time and money. This project work tries to leverage Abstract Interpretation techniques for static analysis of C programs. C Analyzer is a tool developed for static analysis of C programs. This implementation of C Analyzer provides a plug-and-play domain architecture for multiple abstract domains to be used. C Analyzer supports four abstract domains - Interval, Octagon, Polyhedra, and Bit Vector. We use these different domains for required precision in program verification. C Analyzer tool uses LLVM C/C++ compiler frontend Clang API to generate and traverse the Control Flow Graph (CFG) of a given C program. This tool generates invariants in different abstract domains for statements in basic blocks of CFG during CFG traversal. Using these invariants, some properties of a program, such as dividing by zero, modulus zero, arithmetic overflow, etc., can be analyzed. We also use a source-to-source transformation tool, CIL (Common Intermediate language), to transform some C constructs into simpler constructs, such as transforming logical operators, switch statements, and conditional operators into if-else ladders and transforming do-while and for loops into while loops. Using C Analyzer, C program constructs such as declarations, assignments, binary operations (arithmetic, relational, bitwise shift, etc.), conditions (if-else), loops (while, do while, for loop), nested conditions, and nested loops can be analyzed. Currently, this tool does not support arrays, structures, unions, pointers, or function calls.
• Abstract（参考訳）: 私たちの時代には、世界がますますソフトウェアプログラムに依存していくにつれて、バグのない正しいプログラムを書くことが不可欠です。 形式的手法に基づくプログラム検証は、安全クリティカルシステムにおける実行時のエラーを検出し、人間の生活に悪影響を及ぼしたり、時間とお金を節約したりすることで、これを保証できる。 本研究は,Cプログラムの静的解析に抽象解釈技術を活用することを目的とする。 C Analyzerは、Cプログラムの静的解析のために開発されたツールである。 このC Analyzerの実装は、複数の抽象ドメインを使用するためのプラグアンドプレイドメインアーキテクチャを提供する。 C Analyzerは、Interval、Ocagon、Polyhedra、Bit Vectorの4つの抽象ドメインをサポートしている。 プログラム検証において,これらの異なる領域を必要な精度で利用する。 C Analyzerツールは、LLVM C/C++コンパイラのフロントエンドClang APIを使用して、所定のCプログラムの制御フローグラフ(CFG)を生成してトラバースする。 このツールは、CFGトラバーサル中のCFGの基本ブロックのステートメントに対する異なる抽象領域の不変量を生成する。 これらの不変量を用いて、0による割当、モジュラーゼロ、算術オーバーフローなど、プログラムのいくつかの特性を分析することができる。 また、ソースからソースへの変換ツールであるCIL(Common Intermediate Language)を使用して、いくつかのC構造体を論理演算子、スイッチ文、条件演算子をif-elseのラグに変換し、do-whileを変換し、ループを whileループに変換するといった単純な構造に変換する。 C Analyzerを使用すると、Cプログラムは宣言、代入、バイナリ操作(パラメータ、リレーショナル、ビットワイズシフトなど)、条件(if-else)、ループ( while, do while, for loop)、ネスト条件、ネストループなどを生成することができる。 現在、このツールは配列、構造、結合、ポインタ、関数呼び出しをサポートしていない。

関連論文リスト

• Scaling Symbolic Execution to Large Software Systems [0.0]
  シンボル実行は、プログラム検証とバグ検出ソフトウェアの両方で使用される一般的な静的解析手法である。 我々は、Clang Static Analyzerと呼ばれるエラー検出フレームワークと、その周辺に構築されたインフラストラクチャーであるCodeCheckerに焦点を当てた。
  論文  参考訳（メタデータ） (2024-08-04T02:54:58Z)
• FoC: Figure out the Cryptographic Functions in Stripped Binaries with LLMs [54.27040631527217]
  削除されたバイナリの暗号関数を抽出するFoCと呼ばれる新しいフレームワークを提案する。 まず、自然言語における暗号関数のセマンティクスを要約するために、バイナリ大言語モデル(FoC-BinLLM)を構築した。 次に、FoC-BinLLM上にバイナリコード類似モデル(FoC-Sim)を構築し、変更に敏感な表現を作成し、データベース内の未知の暗号関数の類似実装を検索する。
  論文  参考訳（メタデータ） (2024-03-27T09:45:33Z)
• Accurate Coverage Metrics for Compiler-Generated Debugging Information [0.0]
  多くのツールは、プログラム状態のソース言語ビューを示すために、コンパイラが生成したメタデータに依存している。 局所変数のカバー範囲を測定するための現在のアプローチは粗末な仮定に基づいている。 我々は,デバッグ品質を改善するための言語実装のモチベーションとして,ツールによって計算可能な,いくつかの新しいメトリクスを提案する。
  論文  参考訳（メタデータ） (2024-02-07T13:01:28Z)
• LLVM Static Analysis for Program Characterization and Memory Reuse Profile Estimation [0.0]
  本稿ではLLVMに基づく確率的静的解析手法を提案する。 プログラムの特徴を正確に予測し、プログラムの再利用距離プロファイルを推定する。 その結果,LLVMベースの動的コード解析ツールであるByflと比較して,アプリケーションの特性を正確に予測できることがわかった。
  論文  参考訳（メタデータ） (2023-11-20T23:05:06Z)
• A Compiler from Array Programs to Vectorized Homomorphic Encryption [1.6216324006136673]
  ホモモルフィック暗号 (HE) は、暗号化されたデータに対して安全な計算を行うための実践的な手法である。 本稿では,効率的なベクトル化HEプログラムを生成するViaduct-HEを提案する。 Viaduct-HEは、効率的なHEプログラムに必要な操作と複雑なデータレイアウトの両方を生成することができる。
  論文  参考訳（メタデータ） (2023-11-10T16:00:00Z)
• Guess & Sketch: Language Model Guided Transpilation [59.02147255276078]
  学習されたトランスパイレーションは、手作業による書き直しやエンジニアリングの取り組みに代わるものだ。 確率的ニューラルネットワークモデル(LM)は、入力毎に可塑性出力を生成するが、正確性を保証するコストがかかる。 Guess & Sketch は LM の特徴からアライメントと信頼性情報を抽出し、意味的等価性を解決するためにシンボリック・ソルバに渡す。
  論文  参考訳（メタデータ） (2023-09-25T15:42:18Z)
• C-rusted: The Advantages of Rust, in C, without the Disadvantages [0.0]
  C-rustedは、言語、システム、およびユーザ定義リソースのオーナシップ、排他性、共有性を表現するために(部分的に)Cプログラムに注釈を付けることができる革新的な技術である。 注釈付きCプログラムは、ISO Cコードを処理することができるコンパイルツールチェーンの修正されていないバージョンで変換することができる。
  論文  参考訳（メタデータ） (2023-02-10T15:48:09Z)
• 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)
• Representing Partial Programs with Blended Abstract Semantics [62.20775388513027]
  プログラム合成エンジンにおける部分的なプログラム表現手法について紹介する。 モジュラーニューラルネットワークとして実装された近似実行モデルを学ぶ。 これらのハイブリッドニューロシンボリック表現は、実行誘導型シンセサイザーがより強力な言語構成を使うことができることを示す。
  論文  参考訳（メタデータ） (2020-12-23T20:40:18Z)
• Extending C++ for Heterogeneous Quantum-Classical Computing [56.782064931823015]
  qcorはC++とコンパイラの実装の言語拡張で、異種量子古典プログラミング、コンパイル、単一ソースコンテキストでの実行を可能にする。 我々の研究は、量子言語で高レベルな量子カーネル(関数)を表現できる、第一種C++コンパイラを提供する。
  論文  参考訳（メタデータ） (2020-10-08T12:49:07Z)

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

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