Agentic Planning for Symbolic Execution

AGOLIC is an agentic planning system that uses evidence from earlier runs to choose and configure later bounded symbolic execution (BSE) runs, which the underlying symbolic execution tool then carries out. The paper addresses the fundamental limitation of symbolic execution where a practical run may exhaust its resources while much program behaviour remains unreached. To mitigate this, AGOLIC places a planner between bounded symbolic-execution (BSE) runs carried out under assigned resource budgets, allowing the system to reason about how the same tool is utilised from one bounded run to the next, while leaving ordinary state exploration to the underlying tool.

The architecture is designed so that its planning intelligence, available evidence and execution modes can be adapted to the symbolic execution tool and analysis objective. In the specific branch-coverage configuration evaluated, an LLM-based agent reasons over source code, replayed coverage and earlier targeting attempts. The system operates through a round-level procedure where a continuous symbolic-execution run remains active alongside the planner-dispatched runs. At each round, the agent examines replay-derived source-level coverage and the record of earlier BSE attempts to identify program regions that remain underexplored and to formulate new target specifications.

AGOLIC utilizes two primary execution modes:

• Harness-Entry Mode: In this mode, ordinary symbolic exploration begins at the harness.

• Witness-Guided Mode: In this mode, execution under a concrete witness establishes a program state from which ordinary symbolic exploration may resume. This mode is intended for program regions whose setup is expensive to explore symbolically. During pre-release execution, the tool uses the witness to resolve supported input-dependent operations, and at the release-function boundary, ordinary solver-backed symbolic exploration resumes from the reached state.

The system was evaluated on several C and C++ programs and compared against continuous symbolic execution and the other evaluated program-analysis systems, including coverage-guided fuzzing and compilerbased concolic execution. The evaluation results show that On every program, it extends the branch coverage obtained by continuous symbolic execution and covers more than 3× as many branches on average. Additionally, AGOLIC "covers more branches than each individual corpus from coverage-guided fuzzing and compilerbased concolic execution in our evaluation and reaches branches absent from all comparison corpora combined on six of the seven programs."

The authors conclude that these results "point to considerable untapped potential in existing symbolic execution tools, some of which may be realised by reasoning about how their capabilities are used across runs while leaving state selection during ordinary symbolic exploration to the underlying tool."

1. Meta-Cognitive Orchestration for Specialized Toolchains

An AI system that acts as a high-level planner to manage specialized sub-agents (such as formal verifiers, mathematical solvers, or code executors) as bounded execution engines. Instead of attempting to solve complex problems through a single, continuous reasoning chain, the system allocates specific resource budgets to each sub-agent. It analyzes the coverage of the sub-agent's output to identify logical gaps and dynamically re-configures the parameters, constraints, or entry points for the next sub-agent call to explore unreached problem spaces.

2. Witness-Guided State Resumption for Long-Context Reasoning

An AI system capable of bypassing computationally expensive or context-heavy setup phases in complex reasoning tasks. By using witnesses—compact, high-fidelity snapshots of intermediate logical or computational states—the system can inject the agent directly into a specific, deep subspace of a problem. This allows the model to resume reasoning from a highly specific state (e.g., a mid-way point in a complex mathematical proof or a specific state in a software execution) rather than re-processing the entire initial context or harness.

3. Iterative Evidence-Based Goal Re-Specification

A system designed to prevent reasoning exhaustion in open-ended, multi-step tasks. The system operates in discrete rounds, where it treats each reasoning cycle as a bounded attempt. After each round, the agent performs a replay analysis of its own previous attempts and the resulting data to identify underexplored logical regions. It then uses this evidence to formulate new, highly targeted sub-goals for the next round, ensuring that computational resources are steered toward the most productive areas of the problem space.

Symbolic execution seeks to explore feasible program paths, yet a practical run may exhaust its resources while much program behaviour remains unreached. We investigate a complementary way of extending its practical reach by reasoning about how the same tool is utilised from one bounded run to the next, while leaving ordinary state exploration to the underlying tool. We present Agolic, an agentic planning system that uses evidence from earlier runs to choose and configure later bounded symbolic execution (BSE) runs, which the underlying symbolic execution tool then carries out. The planning intelligence, available evidence and execution modes can be adapted to the symbolic execution tool and analysis objective. We evaluate one adaptation for branch-coverage exploration, in which an LLM-based agent reasons over source code, replayed coverage and earlier targeting attempts. We evaluate Agolic on several C and C++ programs. On every program, it extends the branch coverage obtained by continuous symbolic execution and covers more than 3 times as many branches on average. It also covers more branches than each individual corpus from coverage-guided fuzzing and compiler-based concolic execution in our evaluation and reaches branches absent from all comparison corpora combined on six of the seven programs. Taken together, these results point to considerable untapped potential in existing symbolic execution tools, some of which may be realised by reasoning about how their capabilities are used across runs while leaving state selection during ordinary symbolic exploration to the underlying tool.