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]

A separate work observes that 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 that specialized HW/SW symbolic/concolic co-validation approaches have been devised for embedded SW.^[3]

Evidence-supported uses

Processor verification with coverage-guided aging

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. The paper surveys related RISC-V test-generation approaches and notes that these variously leverage constraint-based specification templates, constraint-based coverage requirements, coverage-guided fuzzing techniques, and symbolic execution techniques to find specific inputs.^[4][5]

Mutation-based compliance testing for RISC-V

In a mutation-based compliance testing approach for RISC-V, a mutation operator tailored for the RISC-V ISA is defined in a first step, 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.^[6]

Concolic testing of RISC-V embedded binaries

A VP-based approach enables concolic testing for RISC-V binaries that extensively interact with peripherals. On the technical side, the RISC-V ISS and memory are instrumented to track symbolic constraints alongside the native execution, and a specialized interface is provided to integrate SW models of peripherals that is tailored for the requirements of SystemC-based peripherals. The approach 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.^[7]

Within the broader 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; properties are specified as SW assertions.^[8]

CT is noted to be 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.^[9]

Cross-level RISC-V verification (ISS/RTL co-simulation)

An efficient approach for RISC-V processor verification in an RTL/ISS cross-level setting uses an instruction stream generator that produces an endless and dynamically evolving stream of instructions. This stream is fed in a cross-level co-simulation setup to the reference ISS and the RTL core under test, and the architectural state is compared between both models after each instruction. The approach places no control-flow related restrictions on the instruction stream (infinite loops and trap loops are tolerated because the instruction stream evolves dynamically at runtime), does not require restarts (a single endless stream enables very long test sequences), and achieves high performance via tight ISS/RTL co-simulation with instructions injected directly into the processor fetch interface (over 200 million processed instructions per hour on a standard laptop).^[10]

The ISS/RTL co-simulation idea is also taken up in the coverage-guided aging paper, which leverages an ISS as a functional reference model for the RTL processor under test in a tight co-simulation setting.^[11]

Formal verification of SystemC designs (stateful symbolic simulation)

A stateful symbolic simulation approach for SystemC designs is built on an intermediate verification language (IVL) and integrates three techniques under SystemC simulation semantics:

1. Symbolic execution (SymEx) to reason efficiently about a large number of inputs and exploration paths.
2. Partial order reduction (POR) to prune redundant scheduling sequences of SystemC processes.
3. State subsumption reduction (SSR) to efficiently detect exploration cycles in symbolic explorations.^[12]

While these techniques drastically boost verification efficiency and provide a strong framework for SystemC verification, complex symbolic reasoning remains subject to scalability issues, motivating further optimizations.^[13]

One such optimization is compiled symbolic simulation (CSS), which leverages native execution by integrating the symbolic execution engine with the process scheduler (itself employing POR) into the SystemC design under test and compiling all components into a single binary. Performance can be further boosted via a parallelized exploration algorithm on top of CSS, with a VP-based interrupt controller reported as a case-study.^[14]

Integration with simulation-based techniques

The Herdt et al. overview identifies scalability as a major open challenge for formal verification of both VPs and embedded SW binaries. It proposes investigating domain-specific optimizations and efficient combinations of symbolic execution with state space abstraction and reduction techniques (e.g., stateful symbolic simulation for SystemC) and integrating simulation-based techniques with formal methods (e.g., coverage-guided fuzzing with symbolic simulation) into a single unified verification approach that combines the benefits of both worlds, switching seamlessly at runtime between formal and simulation-based verification techniques to cover the state space deeply and broadly.^[15]

The same overview also observes that existing SW verification methods mainly leverage symbolic execution techniques, reinforcing symbolic execution as a foundational approach in the SW domain.^[16]

Symbolic execution in formal RISC-V verification (broader literature)

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 optimized solver back-ends (e.g., Z3, Yices) for assertion-violation detection in RISC-V control FSMs, and apply symbolic execution together with SMT-based BMC to industrial RISC-V pipelines.^[17]

Related techniques in the public context

Compact symbolic execution

Public context describes compact symbolic execution as a generalization of King's symbolic execution technique. It first analyzes cyclic paths in the control-flow graph of a given program 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 along it), independently from the rest of the program. In a second step it symbolically executes the program with those templates to produce a compact symbolic execution tree. A compact tree always carries the same information in all its leaves as the corresponding classic symbolic execution tree, yet is typically substantially smaller, and there are even programs for which compact trees are finite while classic trees are infinite.^[18]

Speculative symbolic execution

Public context also describes speculative symbolic execution (SSE) as a way to speed up symbolic execution by reducing constraint-solver invocations. At branch statements, the search procedure speculatively explores branches without immediate feasibility checking, and the solver is invoked only after a configured number of speculated branches has accumulated. The cited paper reports 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.^[19]

Scope

The supplied evidence supports symbolic execution as a general analysis technique, a key ingredient of concolic testing, and a foundation for stateful symbolic simulation of SystemC and for cross-level RISC-V verification. It documents several concrete RISC-V-oriented uses and variants, as well as its mention in broader RISC-V formal-verification literature. It does not provide a full algorithmic definition of classic symbolic execution beyond these source-backed descriptions.