Technical Report: A Formal Semantics for Java Symbolic Evaluation using Large-Block Encoding

• URL: http://arxiv.org/abs/2608.04513v2
• Date: Sun, 09 Aug 2026 10:41:13 GMT
• Title: Technical Report: A Formal Semantics for Java Symbolic Evaluation using Large-Block Encoding
• Abstract summary: Symbolic execution is used to find bugs, generate test cases, and provide correctness guarantees.<n>Java Ranger is a path-merging tool for Java programs that progressively transforms imperative Java code toward the language of formal logic.<n>We formalize each of these transformations and prove their soundness with respect to a simplified version of the Java concrete semantics.
• Score: 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.

Related papers

• The Imitation Game: When LLMs Learn to Reason Like Programs via Code-Centric Reasoning Data Synthesis [50.473217152006875]
  MIMIC is a framework that leverages executable code as a rigorous medium for reasoning data synthesis.<n>MIMIC transforms algorithms into verifiable reasoning trajectories through narrative fusion, code-guided test synthesis, and dynamic code instrumentation.<n>Our method significantly elevates accuracy across general reasoning, complex mathematical benchmarks, and fine-grained deterministic tasks.
  arXiv  Detail & Related papers  (2026-09-13T17:04:16Z)
• Is Code Better Than Language for Algorithmic Reasoning [58.86873062890482]
  We show that for tool-augmented language models, comparing natural-language reasoning with code-execution pipelines is difficult because the comparison changes both the intermediate representation and the execution mechanism.<n>We separate these factors with an intermediate intervention: the model expresses its reasoning as executable code, and the language model simulates that code in context to produce an answer.<n>We observe that the intermediate intervention is not meaningfully different from natural-language reasoning (+0.15pp)
  arXiv  Detail & Related papers  (2026-06-14T04:17:21Z)
• SEMBridge: Tagless-Final Program Semantics with Weakest-Precondition and Bounded-Checking Interpretations [0.8557392136621891]
  SEMBridge generates weakest-precondition and bounded-checking interpretations from the same executable object programs.<n>The Python prototype implements a loop-free imperative core with assignments, conditionals, assumptions, and assertions.
  arXiv  Detail & Related papers  (2026-05-29T18:00:06Z)
• Can LLMs Recover Program Semantics? A Systematic Evaluation with Symbolic Execution [1.5377279217726239]
  Obfuscation poses a persistent challenge for software engineering tasks such as program comprehension, maintenance, testing, and vulnerability detection.<n>We investigate whether fine-tuned language models can effectively deobfuscate programs and restore analyzability.
  arXiv  Detail & Related papers  (2025-11-24T13:55:20Z)
• Correctness-Guaranteed Code Generation via Constrained Decoding [11.531496728670746]
  We present a constrained runtime decoding algorithm for generating semantically correct programs.<n>We show that our method can generate semantically correct programs conforming to any prescribed scripting API.<n>We further show that, with careful design, our semantic guarantees extend to correctness, as validated in the application of generating game mechanics for a roguelike video game.
  arXiv  Detail & Related papers  (2025-08-20T20:48:18Z)
• Exposing Go's Hidden Bugs: A Novel Concolic Framework [2.676686591720132]
  We present Zorya, a novel methodology to evaluate Go programs comprehensively.<n>By systematically exploring execution paths to uncover vulnerabilities beyond conventional testing, symbolic execution offers distinct advantages.<n>Our solution employs Ghidra's P-Code as an intermediate representation (IR)
  arXiv  Detail & Related papers  (2025-05-26T16:26:20Z)
• EquiBench: Benchmarking Large Language Models' Reasoning about Program Semantics via Equivalence Checking [58.15568681219339]
  We introduce EquiBench, a new benchmark for evaluating large language models (LLMs)<n>This task directly tests a model's ability to reason about program semantics.<n>We evaluate 19 state-of-the-art LLMs and find that in the most challenging categories, the best accuracies are 63.8% and 76.2%, only modestly above the 50% random baseline.
  arXiv  Detail & Related papers  (2025-02-18T02:54:25Z)
• ReF Decompile: Relabeling and Function Call Enhanced Decompile [50.86228893636785]
  The goal of decompilation is to convert compiled low-level code (e.g., assembly code) back into high-level programming languages.<n>This task supports various reverse engineering applications, such as vulnerability identification, malware analysis, and legacy software migration.
  arXiv  Detail & Related papers  (2025-02-17T12:38:57Z)
• Weakly Supervised Semantic Parsing with Execution-based Spurious Program Filtering [19.96076749160955]
  We propose a domain-agnostic filtering mechanism based on program execution results. We run a majority vote on these representations to identify and filter out programs with significantly different semantics from the other programs.
  arXiv  Detail & Related papers  (2023-11-02T11:45:40Z)
• Guess & Sketch: Language Model Guided Transpilation [59.02147255276078]
  Learned transpilation offers an alternative to manual re-writing and engineering efforts. Probabilistic neural language models (LMs) produce plausible outputs for every input, but do so at the cost of guaranteed correctness. Guess & Sketch extracts alignment and confidence information from features of the LM then passes it to a symbolic solver to resolve semantic equivalence.
  arXiv  Detail & Related papers  (2023-09-25T15:42:18Z)
• Natural Language to Code Translation with Execution [82.52142893010563]
  Execution result--minimum Bayes risk decoding for program selection. We show that it improves the few-shot performance of pretrained code models on natural-language-to-code tasks.
  arXiv  Detail & Related papers  (2022-04-25T06:06:08Z)
• ReACC: A Retrieval-Augmented Code Completion Framework [53.49707123661763]
  We propose a retrieval-augmented code completion framework, leveraging both lexical copying and referring to code with similar semantics by retrieval. We evaluate our approach in the code completion task in Python and Java programming languages, achieving a state-of-the-art performance on CodeXGLUE benchmark.
  arXiv  Detail & Related papers  (2022-03-15T08:25:08Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.