Symbolic Execution
TechniqueIn the supplied evidence, symbolic execution is described as a path-oriented, constraint-based program analysis technique. The evidence shows it being used for ISS/RTL co-simulation in processor verification, for selective exploration in hardware fuzzing (FuSS), and for leakage-trace generation in a leakage-contract verification pipeline. Public context also describes compact symbolic execution and speculative symbolic execution as related techniques.
First seen 5/25/2026
Last seen 7/16/2026
Evidence 43 chunks
Wiki v2
WIKI
Overview
In the supplied evidence, symbolic execution is described as a path-oriented, constraint-based program analysis technique.[1]
Evidence-supported uses
NEIGHBORHOOD
No graph connections found for this entity yet. It may appear in future ingestion runs.
explore full graph →RELATIONSHIPS
24 connectionsThe paper proposes leveraging symbolic execution techniques for processor verification.
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.
Examiner uses symbolic execution on ARM ASL code to generate test cases.
ATGen uses constraint logic programming and symbolic execution for structural coverage.
The paper implements the first symbolic execution engine for ARM ASL to generate test cases.
Cross-level processor verification is enabled by symbolic execution.
Symbolic execution is applied to implement processor verification at the RTL.
KLEE is a state-of-the-art symbolic execution engine used to implement 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.
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
Symbolic execution transforms program states represented by environment, heap, and constraints.
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.
Whitebox fuzzing is implemented using symbolic execution.
LINKED ENTITIES
3 linksClosing the Gap: Leakage Contracts for Processors with Transitions and Glitches USES Extracted graph relationship
FuSS: Coverage-Directed Hardware Fuzzing with Selective Symbolic Execution USED_BY FuSS uses symbolic execution selectively to break a coverage plateau after fuzzing.
Processor Verification using Symbolic Execution: A RISC-V Case-Study USED_BY The case study uses symbolic execution together with co-simulation for cross-level processor verification.
CITATIONS
9 sources9 citations — click to expand
[1] Symbolic execution is described as a path-oriented, constraint-based program analysis technique. Speculative Symbolic Execution
[2] A RISC-V case study uses symbolic execution in combination with ISS/RTL co-simulation for cross-level processor verification. Processor Verification using Symbolic Execution: A RISC-V Case Study
[3] FuSS is a hardware fuzzing framework that combines design instrumentation, fuzzing until a coverage plateau, hardware-program context mapping, source/destination extraction, and symbolic execution. FuSS: Coverage-Directed Hardware Fuzzing with Selective Symbolic Execution
[4] In FuSS, the symbolic execution manager requires an execution start point, an execution endpoint, and a start state taken from concrete simulation of the fuzzer-generated program. FuSS: Coverage-Directed Hardware Fuzzing with Selective Symbolic Execution
[5] In the leakage-contract pipeline, random shares and masks are symbolic while other initial-state values are concrete, and the contract is symbolically executed to generate a leakage trace. Closing the Gap: Leakage Contracts for Processors with Transitions and Glitches
[6] The symbolic leakage trace is a sequence of leaks represented as computation trees with secrets, masks, and constants as leaf nodes, and tracing granularity is user-defined for bit-sliced or n-sliced implementations. Closing the Gap: Leakage Contracts for Processors with Transitions and Glitches
[7] The leakage-contract paper verifies t-probing security by constructing correlation sets and translating the result into a single SAT problem. Closing the Gap: Leakage Contracts for Processors with Transitions and Glitches
[8] Compact symbolic execution generalizes King's symbolic execution by analyzing cyclic CFG paths to compute templates and produce smaller or finite symbolic execution trees. Compact Symbolic Execution
[9] Speculative symbolic execution reduces constraint-solver invocations by speculatively exploring branches and invoking the solver only after a configured number of branches has accumulated, with reported reductions in solver invocations and search time. Speculative Symbolic Execution