Symbolic Execution
TechniqueSymbolic execution is described in the supplied evidence as a path-oriented, constraint-based program analysis technique. The evidence documents its use in processor verification (notably RISC-V case-studies), mutation-based compliance testing for RISC-V, concolic testing of embedded RISC-V binaries, and as a building block of stateful symbolic simulation for SystemC designs. Public context also describes compact and speculative variants of symbolic execution.
First seen 5/25/2026
Last seen 9/28/2026
Evidence 51 chunks
Wiki v4
WIKI
Overview
In the supplied evidence, symbolic execution is described as a path-oriented, constraint-based program analysis technique.[1]
A related variant, concolic testing (CT), works by tracking symbolic constraints on top of concrete execution and solving these constraints to generate new inputs that explore new program paths and maximize SW path coverage; the same constraints are also leveraged to check assertions and other potential error conditions alongside execution.[2]
NEIGHBORHOOD
4 nodes · 4 edgesgraph · Symbolic Execution · depth=1
RELATIONSHIPS
32 connectionsThe title indicates symbolic execution is the method applied for processor verification.
The paper implements the first symbolic execution engine for ARM ASL to generate test cases.
ATGen uses constraint logic programming and symbolic execution for structural coverage.
Symbolic execution is applied to implement processor verification at the RTL.
Cross-level processor verification is enabled by symbolic execution.
Examiner uses symbolic execution on ARM ASL code to generate test cases.
The paper proposes using symbolic execution as the basis for test case generation.
Test case generation is performed via symbolic execution of CLP-translated programs.
Symbolic execution in the framework includes special support for dynamic memory allocation.
Cited as employing symbolic execution to find specific inputs in the context of RISC-V verification.
KLEE is a state-of-the-art symbolic execution engine used to implement symbolic execution.
Cross-level processor verification via endless randomized instruction stream generation with coverage-guided aging ← compares with 75% 1e
The paper mentions symbolic execution as a related approach
Angr targets binary level symbolic execution
Whitebox fuzzing is implemented using symbolic execution.
The paper uses symbolic execution to replace unknown values by constraint variables.
Symbolic execution follows execution paths by replacing values with constraint variables.
Symbolic execution replaces unknown values with constraint variables.
Symbolic execution transforms program states represented by environment, heap, and constraints.
Stateful symbolic simulation integrates symbolic execution as one of its core techniques
Concolic testing tracks symbolic constraints on top of concrete execution
The paper mentions symbolic execution as a technique to find specific inputs in related work.
S2E targets binary level symbolic execution
Symbolic execution is contrasted with fuzzing, noted as a formal technique that can explore large state spaces more efficiently.
Path explosion is a known challenge in symbolic execution, but is not an issue in this context due to limited ASL constraints.
Symbolic execution is applied to the contract to produce leak sequences.
AVPGEN uses symbolic execution as a novel concept to generate effective tests.
Symbolic execution is used alongside assertions to simulate different paths triggered by the testbench.
Symbolic execution uses symbolic expressions to represent sets of concrete values.
The review covers symbolic execution as one of the scalable formal verification approaches for RISC-V control logic.
The paper uses a hybrid method combining symbolic execution with model checking for RISC-V cores.
KLEE made symbolic execution techniques applicable to large software
SAGE made symbolic execution techniques applicable to large software
CITATIONS
18 sources18 citations — click to expand
[1] Symbolic execution is described as a path-oriented, constraint-based program analysis technique. Speculative Symbolic Execution
[2] Concolic testing works by tracking symbolic constraints on top of concrete execution and solving these constraints to generate new inputs that explore new program paths and maximize SW path coverage; the same constraints are also leveraged to check assertions and other potential error conditions alongside execution. Advanced virtual prototyping for cyber-physical systems
[3] Symbolic execution techniques have been scaled to large SW by systems such as KLEE and SAGE, with subsequent work focusing on binary-level SW to obtain accurate results (e.g., S2E, Mayhem, Angr), and specialized HW/SW symbolic/concolic co-validation approaches have been devised for embedded SW. Advanced virtual prototyping for cyber-physical systems
[4] A RISC-V case study (MINRES The Good Core / TGC series) builds on a randomized coverage-guided instruction stream generator and tight ISS/RTL co-simulation, and uses coverage-guided aging to smooth out the coverage distribution of the randomized instruction stream over time; related RISC-V test-generation approaches leverage constraint-based specification templates, constraint-based coverage requirements, coverage-guided fuzzing techniques, and symbolic execution techniques to find specific inputs. RISC-V Processor Verification with Coverage-guided Aging
[5] In a mutation-based compliance testing approach for RISC-V, a mutation operator tailored for the RISC-V ISA is defined first, and in a second step symbolic execution techniques are leveraged to generate a test-suite that kills all mutations in the ISS that implements the RISC-V ISA. Advanced virtual prototyping for cyber-physical systems
[6] A VP-based approach enables concolic testing for RISC-V binaries that extensively interact with peripherals; the RISC-V ISS and memory are instrumented to track symbolic constraints alongside native execution, with a specialized interface for SystemC-based peripherals, and has been effective in finding buffer overflows in the TCP/IP stack of FreeRTOS and a bug in the RISC-V-specific memcpy of newlib. Advanced virtual prototyping for cyber-physical systems
[7] Within the VP-based verification framework, the test generator continuously provides new inputs to the execution engine, symbolic constraints are traced alongside VP-based execution and are used to drive automated test generation tailored to increase coverage for functional verification, and properties are specified as SW assertions. Advanced virtual prototyping for cyber-physical systems
[8] CT is susceptible to scalability issues due to path explosion and complex symbolic constraints, motivating scalable simulation-based methods such as coverage-guided fuzzing to complement it. Advanced virtual prototyping for cyber-physical systems
[9] An efficient approach for RISC-V processor verification in an RTL/ISS cross-level setting uses an instruction stream generator producing an endless, dynamically evolving instruction stream fed in cross-level co-simulation to the reference ISS and RTL core under test, with architectural state compared after each instruction, no control-flow restrictions, no restarts, and over 200 million processed instructions per hour via tight ISS/RTL co-simulation with instructions injected into the processor fetch interface. Advanced virtual prototyping for cyber-physical systems
[10] The coverage-guided aging paper leverages an ISS as a functional reference model for the RTL processor under test in a tight co-simulation setting. RISC-V Processor Verification with Coverage-guided Aging
[11] A stateful symbolic simulation approach for SystemC designs is built on an intermediate verification language (IVL) and integrates symbolic execution (SymEx) to reason efficiently about a large number of inputs and exploration paths, partial order reduction (POR) to prune redundant scheduling sequences, and state subsumption reduction (SSR) to efficiently detect exploration cycles in symbolic explorations. Advanced virtual prototyping for cyber-physical systems
[12] While the SymEx+POR+SSR techniques drastically boost verification efficiency for SystemC, complex symbolic reasoning remains subject to scalability issues, motivating further optimizations. Advanced virtual prototyping for cyber-physical systems
[13] Compiled symbolic simulation (CSS) leverages native execution by integrating the symbolic execution engine with the process scheduler (using POR) into the SystemC design under test and compiling all components into a single binary, with performance further boosted via a parallelized exploration algorithm; a VP-based interrupt controller is reported as a case-study. Advanced virtual prototyping for cyber-physical systems
[14] The Herdt et al. overview identifies scalability as a major open challenge for formal verification of both VPs and embedded SW binaries, proposing efficient combinations of symbolic execution with state space abstraction and reduction techniques and integration of simulation-based techniques with formal methods into a single unified verification approach that switches seamlessly at runtime between formal and simulation-based verification techniques. Advanced virtual prototyping for cyber-physical systems
[15] The same overview observes that existing SW verification methods mainly leverage symbolic execution techniques, reinforcing symbolic execution as a foundational approach in the SW domain. Advanced virtual prototyping for cyber-physical systems
[16] A review of scalable formal verification strategies for RISC-V-based control paths cites works that embed symbolic execution trees in proof assistants for ISA-level verification, combine symbolic execution with bounded model checking (BMC) using solver back-ends such as Z3 and Yices for assertion-violation detection in RISC-V control FSMs, and apply symbolic execution together with SMT-based BMC to industrial RISC-V pipelines. Scalable Formal Verification Strategies for RISC-V Based Control Paths: A Review
[17] Compact symbolic execution is a generalization of King's symbolic execution technique; it first analyzes cyclic paths in the control-flow graph to compute a template (a declarative parametric description of all possible program states that may leave the analyzed cyclic path after any number of iterations), then symbolically executes the program with those templates to produce a compact symbolic execution tree, which is typically substantially smaller than the corresponding classic tree and can be finite where the classic tree is infinite. Compact Symbolic Execution
[18] Speculative symbolic execution (SSE) speeds up symbolic execution by reducing constraint-solver invocations: at branch statements, the search procedure speculatively explores branches without immediate feasibility checking, invoking the solver only after a configured number of speculated branches has accumulated, with reported reductions in solver invocations (21–49%, averaging 30%) and search-time savings (23.6%–43.6%, averaging 30%) on Symbolic Pathfinder (SPF) across six programs. Speculative Symbolic Execution