論文の概要: Desyan: A Platform for Seamless Value-Flow and Symbolic Analysis
- arxiv url: http://arxiv.org/abs/2508.00508v1
- Date: Fri, 01 Aug 2025 10:39:09 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-08-04 18:08:53.836842
- Title: Desyan: A Platform for Seamless Value-Flow and Symbolic Analysis
- Title（参考訳）: Desyan: シームレスなバリューフローとシンボリック分析のためのプラットフォーム
- Authors: Panagiotis Diamantakis, Thanassis Avgerinos, Yannis Smaragdakis,
- Abstract要約: Desyanは、バリューフローとシンボリック推論をシームレスに統合したプログラム分析を書くためのプラットフォームである。
バリューフロー解析では、エンジンはクラスで最高のデータログ評価器である。
完全なSMTを必要とするアプリケーションに対しては、エンジンは主要なSMTソルバを活用している。
- 参考スコア（独自算出の注目度）: 1.7205106391379026
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Over the past two decades, two different types of static analyses have emerged as dominant paradigms both in academia and industry: value-flow analysis (e.g., data-flow analysis or points-to analysis) and symbolic analysis (e.g., symbolic execution). Despite their individual successes in numerous application fields, the two approaches have remained largely separate; an artifact of the simple reality that there is no broadly adopted unifying platform for effortless and efficient integration of symbolic techniques with high-performance data-flow reasoning. To bridge this gap, we introduce Desyan: a platform for writing program analyses with seamless integration of value-flow and symbolic reasoning. Desyan expands a production-ready Datalog fixpoint engine (Souffl\'e) with full-fledged SMT solving invoking industry-leading SMT engines. Desyan provides constructs for automatically (and efficiently!) handling typical patterns that come up in program analysis. At the same time, the integration is agnostic with respect to the solving technology, and supports Datalog-native symbolic reasoning, via a bottom-up algebraic reasoning module. The result is an engine that allows blending different kinds of reasoning, as needed for the underlying analysis. For value-flow analysis, the engine is the best-in-class Datalog evaluator (often by a factor of over 20x in execution time); for applications that require full SMT (e.g., a concolic execution engine or other symbolic evaluator that needs to solve arbitrarily complex conditions), the engine is leveraging the leading SMT solvers; for lightweight symbolic evaluation (e.g., solving simple conditionals in the context of a path-sensitive analysis), the engine can use Datalog-native symbolic reasoning, achieving large speedups (often of over 2x) compared to eagerly appealing to an SMT solver.
- Abstract（参考訳）: 過去20年間で、価値フロー分析(例えば、データフロー分析やポイントツー分析)とシンボリック分析(例えば、シンボリック実行)という、2つの異なるタイプの静的分析が、学術と産業の両方において支配的なパラダイムとして登場した。
単純な現実の成果として、高性能なデータフロー推論によるシンボリックテクニックの効率的かつ効率的な統合のための統一プラットフォームが広く採用されていない。
このギャップを埋めるために、我々はDesyanを紹介します。これは、バリューフローとシンボリック推論をシームレスに統合したプログラム分析を書くためのプラットフォームです。
Desyanはプロダクション対応のDatalogフィクスポイントエンジン(Souffl\'e)を拡張し、業界主導のSMTエンジンを本格的なSMTで解決する。
Desyanは、プログラム分析に現れる典型的なパターンを自動的に(そして効率的に!
同時に、この統合は問題解決技術に関して非依存であり、ボトムアップ代数的推論モジュールを通じて、Datalogネイティブのシンボル推論をサポートする。
その結果、基礎となる分析に必要なように、異なる種類の推論をブレンドできるエンジンが実現した。
バリューフロー解析では、エンジンは最高レベルのデータログ評価器(多くの場合、実行時間の20倍以上)であり、完全なSMTを必要とするアプリケーション(例えば、衝突実行エンジンや任意の複雑な条件を解く必要がある記号評価器)では、エンジンは主要なSMTソルバを活用している。
関連論文リスト
- FABLE: A Novel Data-Flow Analysis Benchmark on Procedural Text for Large Language Model Evaluation [5.866040886735852]
FABLEは、構造化された手続き型テキストを用いて、大規模言語モデルのデータフロー理解を評価するために設計されたベンチマークである。
推論中心モデル(DeepSeek-R1 8B)、汎用モデル(LLaMA 3.1 8B)、コード固有モデル(Granite Code 8B)の3種類を評価した。
その結果,推理モデルでは精度が向上するが,他のモデルに比べて20倍以上の推論が遅くなることがわかった。
論文 参考訳（メタデータ） (2025-05-30T06:32:34Z) - Pangu Embedded: An Efficient Dual-system LLM Reasoner with Metacognition [95.54406667705999]
Pangu Embeddedは、Ascend Neural Processing Units (NPU) 上で開発された効率的なLarge Language Model (LLM) 推論器である。
既存の推論最適化 LLM でよく見られる計算コストと推論遅延の問題に対処する。
単一の統一モデルアーキテクチャ内で、迅速な応答と最先端の推論品質を提供する。
論文 参考訳（メタデータ） (2025-05-28T14:03:02Z) - Manalyzer: End-to-end Automated Meta-analysis with Multi-agent System [48.093356587573666]
メタアナリシス(Meta-analysis)は、複数の既存の研究からデータを合成し、包括的な結論を導き出す体系的な研究手法である。
伝統的なメタ分析は、文献検索、紙のスクリーニング、データ抽出を含む複雑な多段階パイプラインを含む。
本稿では,ツールコールによるエンドツーエンドの自動メタ分析を実現するマルチエージェントシステムManalyzerを提案する。
論文 参考訳（メタデータ） (2025-05-22T07:25:31Z) - Universal Scalability in Declarative Program Analysis (with Choice-Based Combination Pruning) [1.3874486202578669]
選択構成が述語の評価を柔軟に制限できる準ユニバーサル構成を示す。
我々はこの手法を、おそらく現存する最大の既存のデータログ分析フレームワークに適用する: Doop(Javaコード用)とGigahorseフレームワークからのメインクライアント分析。
論文 参考訳（メタデータ） (2025-03-07T21:23:02Z) - Matchmaker: Self-Improving Large Language Model Programs for Schema Matching [60.23571456538149]
本稿では,スキーママッチングのための合成言語モデルプログラムを提案する。
Matchmakerは、ラベル付きデモを必要とせずに、ゼロショットで自己改善する。
実証的に、Matchmakerが以前のMLベースのアプローチより優れている実世界の医療スキーママッチングベンチマークを実証する。
論文 参考訳（メタデータ） (2024-10-31T16:34:03Z) - LogParser-LLM: Advancing Efficient Log Parsing with Large Language Models [19.657278472819588]
LLM機能と統合された新しいログであるLog-LLMを紹介する。
粒度を解析する複雑な課題に対処し、ユーザが特定のニーズに合わせて粒度を調整できるようにするための新しい指標を提案する。
提案手法の有効性は,Loghub-2kと大規模LogPubベンチマークを用いて実験的に検証した。
論文 参考訳（メタデータ） (2024-08-25T05:34:24Z) - LLMDFA: Analyzing Dataflow in Code with Large Language Models [8.92611389987991]
本稿では,コンパイル不要でカスタマイズ可能なデータフロー解析フレームワークLLMDFAを提案する。
問題をいくつかのサブタスクに分解し、一連の新しい戦略を導入する。
LLMDFAは平均87.10%の精度と80.77%のリコールを達成し、F1スコアを最大0.35に向上させた。
論文 参考訳（メタデータ） (2024-02-16T15:21:35Z) - GEqO: ML-Accelerated Semantic Equivalence Detection [3.5521901508676774]
クラスタリソースの効率的な利用とジョブ実行時間の削減には,共通計算が不可欠だ。
大規模分析エンジンの等価性を検出するには、完全に自動化された効率的でスケーラブルなソリューションが必要である。
本稿では,大規模で意味論的に等価な計算を効率的に識別する,ポータブルで軽量な機械学習ベースのフレームワークであるGEqOを提案する。
論文 参考訳（メタデータ） (2024-01-02T16:37:42Z) - Analytical Engines With Context-Rich Processing: Towards Efficient
Next-Generation Analytics [12.317930859033149]
我々は、文脈に富む分析を可能にするコンポーネントと協調して最適化された分析エンジンを構想する。
我々は、リレーショナルおよびモデルベース演算子間の総括的なパイプラインコストとルールベースの最適化を目指している。
論文 参考訳（メタデータ） (2022-12-14T21:46:33Z) - Linear Temporal Logic Modulo Theories over Finite Traces (Extended
Version) [72.38188258853155]
有限トレース(LTLf)上の線形時間論理について検討する。
命題の文字は任意の理論で解釈された一階述語式に置き換えられる。
Satisfiability Modulo Theories (LTLfMT) と呼ばれる結果の論理は半決定可能である。
論文 参考訳（メタデータ） (2022-04-28T17:57:33Z) - High-performance symbolic-numerics via multiple dispatch [52.77024349608834]
Symbolics.jlは拡張可能なシンボルシステムで、動的多重ディスパッチを使用してドメインのニーズに応じて振る舞いを変更する。
実装に依存しないアクションでジェネリックapiを形式化することで、システムに最適化されたデータ構造を遡及的に追加できることを示します。
従来の用語書き換えシンプリファイアと電子グラフベースの用語書き換えシンプリファイアをスワップする機能を実証する。
論文 参考訳（メタデータ） (2021-05-09T14:22:43Z) - Self-Supervised Log Parsing [59.04636530383049]
大規模ソフトウェアシステムは、大量の半構造化ログレコードを生成する。
既存のアプローチは、ログ特化や手動ルール抽出に依存している。
本稿では,自己教師付き学習モデルを用いて解析タスクをマスク言語モデリングとして定式化するNuLogを提案する。
論文 参考訳（メタデータ） (2020-03-17T19:25:25Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。