論文の概要: Technical Report: A Formal Semantics for Java Symbolic Evaluation using Large-Block Encoding

• arxiv url: http://arxiv.org/abs/2608.04513v1
• Date: Wed, 05 Aug 2026 06:49:28 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-08-06 14:48:43.763168
• Title: Technical Report: A Formal Semantics for Java Symbolic Evaluation using Large-Block Encoding
• Title（参考訳）: 技術的報告:大ブロックエンコーディングを用いたJavaシンボル評価のための形式的セマンティクス
• Authors: Soha Hussein, Stephen McCamant, Kelton OBrien, Kuen-Bang Hou, Michael Whalen, Vaibhav Sharma,
• Abstract要約: シンボリック実行はバグを見つけ、テストケースを生成し、正確性を保証するために使用される。 Java Rangerは、命令型Javaコードを形式論理の言語に段階的に変換するJavaプログラムのためのパスマージツールである。 これらの変換を形式化し、Javaの具体的セマンティクスの簡易バージョンに関して、それらの健全性を証明します。
• 参考スコア（独自算出の注目度）: 0.9985222473972001
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: Symbolic execution plays a critical role in software reliability, as they are used to find bugs, generate test cases, and provide correctness guarantees, particularly for safety-critical systems. Yet their own correctness is rarely subject to formal scrutiny, as it is typically established empirically by evaluating tool behavior across many programs. This leaves open the possibility that the tools themselves introduce unsoundness, potentially invalidating the verification results they produce and undermining the very guarantees they are meant to provide. In this paper, we address this gap by providing the formal treatment of symbolic execution with path-merging, an optimization that improves path explosion by summarizing branching code regions into disjunctive constraints rather than exploring each path independently. Specifically, we target Java Ranger, a path-merging tool for Java programs that progressively transforms imperative Java code toward the language of formal logic through a series of code transformations. We formalize each of these transformations and prove their soundness with respect to a simplified version of the Java concrete semantics, establishing that Java Ranger's path-merging process preserves program semantics.
• Abstract（参考訳）: シンボリック実行は、バグを見つけ、テストケースを生成し、特に安全クリティカルなシステムに対して正確性を保証するために使用されるため、ソフトウェアの信頼性において重要な役割を果たす。 しかし、それら自身の正しさが形式的な精査の対象になることは滅多になく、多くのプログラムでツールの振る舞いを評価することによって実証的に確立されるのが一般的である。 このことは、ツール自体が不健全性を導入し、それらが生成する検証結果を無効にし、提供するはずの確証を損なう可能性があることを物語っている。 本稿では,各経路を独立に探索するのではなく,分岐するコード領域を解離制約にまとめることで,経路の爆発を改善する最適化であるパスマージによるシンボル実行の形式的処理を提供することにより,このギャップに対処する。 具体的には、命令型Javaコードを一連のコード変換を通じて形式論理の言語に段階的に変換するJavaプログラム用のパスマージツールであるJava Rangerをターゲットにしています。 我々はこれらの変換を形式化し、Javaの具体的意味論の簡易バージョンに関してそれらの健全性を証明し、Java Rangerのパスマージプロセスがプログラムの意味論を保存することを確証する。

関連論文リスト

• Is Code Better Than Language for Algorithmic Reasoning [58.86873062890482]
  ツール拡張言語モデルでは、中間表現と実行機構の両方を変えるため、自然言語推論とコード実行パイプラインを比較することは困難である。 モデルは、その推論を実行可能なコードとして表現し、言語モデルは、そのコードを文脈でシミュレートして、回答を生成する。 中間介入は自然言語の推論と有意に異なるものではない(+0.15pp)。
  論文  参考訳（メタデータ） (2026-06-14T04:17:21Z)
• SEMBridge: Tagless-Final Program Semantics with Weakest-Precondition and Bounded-Checking Interpretations [0.8557392136621891]
  SEMBridgeは、同じ実行可能なオブジェクトプログラムから最も弱い条件と境界チェックの解釈を生成する。 Pythonプロトタイプは、割り当て、条件、仮定、アサーションを備えたループフリーな命令コアを実装している。
  論文  参考訳（メタデータ） (2026-05-29T18:00:06Z)
• Can LLMs Recover Program Semantics? A Systematic Evaluation with Symbolic Execution [1.5377279217726239]
  難読化は、プログラムの理解、メンテナンス、テスト、脆弱性検出といったソフトウェアエンジニアリングタスクに永続的な課題をもたらす。 微調整言語モデルがプログラムを効果的に難読化し、分析可能性を取り戻すことができるかどうかを検討する。
  論文  参考訳（メタデータ） (2025-11-24T13:55:20Z)
• Correctness-Guaranteed Code Generation via Constrained Decoding [11.531496728670746]
  本稿では,意味論的に正しいプログラムを生成するための制約付き実行時復号アルゴリズムを提案する。 提案手法は,任意の所定のスクリプティングAPIに従って,意味的に正しいプログラムを生成することができることを示す。 さらに、慎重に設計することで、我々のセマンティック保証が正当性にまで拡張され、ローグライクなビデオゲームにゲームメカニクスを発生させることで検証されることを示す。
  論文  参考訳（メタデータ） (2025-08-20T20:48:18Z)
• Exposing Go's Hidden Bugs: A Novel Concolic Framework [2.676686591720132]
  本稿では,Goプログラムを包括的に評価する新しい方法論であるZoryaを紹介する。 従来のテスト以上の脆弱性を明らかにするために、システミックに実行パスを探索することで、象徴的な実行には明確なメリットがある。 我々の解は、GhidraのP-Codeを中間表現(IR)として採用する。
  論文  参考訳（メタデータ） (2025-05-26T16:26:20Z)
• EquiBench: Benchmarking Large Language Models' Reasoning about Program Semantics via Equivalence Checking [58.15568681219339]
  大規模言語モデル(LLM)を評価するための新しいベンチマークであるEquiBenchを紹介する。 このタスクは、プログラムのセマンティクスについて推論するモデルの能力を直接テストする。 19の最先端LCMを評価し、最も難しいカテゴリでは、最高の精度は63.8%と76.2%であり、50%のランダムベースラインよりわずかに高い。
  論文  参考訳（メタデータ） (2025-02-18T02:54:25Z)
• ReF Decompile: Relabeling and Function Call Enhanced Decompile [50.86228893636785]
  逆コンパイルの目標は、コンパイルされた低レベルコード(アセンブリコードなど)を高レベルプログラミング言語に変換することである。 このタスクは、脆弱性識別、マルウェア分析、レガシーソフトウェアマイグレーションなど、さまざまなリバースエンジニアリングアプリケーションをサポートする。
  論文  参考訳（メタデータ） (2025-02-17T12:38:57Z)
• Weakly Supervised Semantic Parsing with Execution-based Spurious Program Filtering [19.96076749160955]
  本稿では,プログラムの実行結果に基づくドメインに依存しないフィルタリング機構を提案する。 私たちはこれらの表現に対して多数決を行い、他のプログラムと大きく異なる意味を持つプログラムを特定し、フィルタリングします。
  論文  参考訳（メタデータ） (2023-11-02T11:45:40Z)
• Guess & Sketch: Language Model Guided Transpilation [59.02147255276078]
  学習されたトランスパイレーションは、手作業による書き直しやエンジニアリングの取り組みに代わるものだ。 確率的ニューラルネットワークモデル(LM)は、入力毎に可塑性出力を生成するが、正確性を保証するコストがかかる。 Guess & Sketch は LM の特徴からアライメントと信頼性情報を抽出し、意味的等価性を解決するためにシンボリック・ソルバに渡す。
  論文  参考訳（メタデータ） (2023-09-25T15:42:18Z)
• Natural Language to Code Translation with Execution [82.52142893010563]
  実行結果-プログラム選択のための最小ベイズリスク復号化。 そこで本研究では,自然言語からコードへのタスクにおいて,事前訓練されたコードモデルの性能を向上することを示す。
  論文  参考訳（メタデータ） (2022-04-25T06:06:08Z)

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

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