Concolic Testing

Technique

Concolic testing is a hybrid software and hardware verification technique that combines concrete execution with symbolic constraint tracking. By solving symbolic constraints, it systematically generates new inputs that steer execution along unexplored paths to maximize code coverage and expose bugs. The method has been adapted from general-purpose software into specialized settings such as logic programming, embedded RISC-V binaries analyzed through virtual prototypes, and RTL hardware designs, while known limitations include the path-explosion problem and scalability challenges on complex programs.

First seen 5/29/2026

Last seen 9/28/2026

Evidence 13 chunks

Wiki v1

WIKI

Overview

Concolic testing (CT) is a verification technique that fuses concrete execution with symbolic execution. As a program runs concretely, CT records symbolic constraints on inputs along each branch. By negating selected constraints and invoking a constraint solver, CT produces new concrete inputs that drive execution down previously unexplored paths. The technique is widely used to maximize code coverage, activate hard-to-reach branches, expose assertion violations, and generate test suites that exercise different program behaviors (citation: Abstraction-driven Concolic Testing; LLM4DV; Sci China Inf Sci 2022, §6.1).

Core Mechanism

READ FULL ARTICLE →

NEIGHBORHOOD

5 nodes · 6 edges

graph · Concolic Testing · depth=1

RELATIONSHIPS

12 connections

RVX ← implements 100% 2e

The title explicitly characterizes RVX as a tool for concolic testing.

RTL uses → 95% 1e

Concolic testing analyzes RTL designs to generate effective test sequences.

DeepVerifier: Learning to Update Test Sequences for Coverage-Guided Verification ← compares with 85% 1e

The paper discusses concolic testing as a competing semi-formal method for test generation.

Processor Verification using Symbolic Execution: A RISC-V Case-Study ← mentions 85% 1e

The paper mentions concolic testing on RTL models as related work.

LLM4DV ← mentions 93% 1e

The paper mentions concolic testing as a prior approach to test generation in hardware verification.

Advanced Virtual Prototyping for Cyber-Physical Systems Using RISC-V ← uses 100% 1e

The paper presents concolic testing as one of the VP-based verification approaches

Symbolic Execution uses → 100% 1e

Concolic testing tracks symbolic constraints on top of concrete execution

RISC-V VP ← uses 100% 1e

The RISC-V VP is used as execution engine for concolic testing of embedded SW

Coverage-Guided Fuzzing (CGF) compares with → 90% 1e

CGF is presented as a scalable complement to concolic testing

DeepVerifier: Learning to Update Test Sequences for Coverage-Guided Verification ← mentions 100% 1e

The paper mentions concolic testing as a semi-formal verification method.

control flow graph uses → 95% 1e

Concolic testing generates test sequences by analyzing the control flow graph of RTL designs.

RVX-a tool for concolic testing of embedded binaries targeting RISC-V platforms ← uses 90% 1e

RVX is introduced as a tool specifically for concolic testing, indicating the paper’s technical focus.

LINKED ENTITIES

2 links

RVX-a tool for concolic testing of embedded binaries targeting RISC-V platforms USES Extracted graph relationship

RVX IMPLEMENTS Extracted graph relationship

CITATIONS

9 sources

9 citations — click to expand

[1] Concolic testing is a hybrid verification technique that combines concrete execution with symbolic constraint tracking, using a constraint solver to generate new inputs that steer execution along unexplored paths. Advanced virtual prototyping for cyber-physical systems using RISC-V: implementation, verification and challenges (Herdt & Drechsler, Sci China Inf Sci 2022)

[2] The RVX tool instruments the RISC-V ISS and memory to track symbolic constraints alongside native execution and provides a specialized interface for SystemC-based peripheral models, enabling concolic testing of embedded binaries that extensively interact with peripherals. Advanced virtual prototyping for cyber-physical systems using RISC-V (Sci China Inf Sci 2022, §6.1)

[3] RVX was effective in finding buffer overflows in the TCP/IP stack of FreeRTOS and a bug in the RISC-V specific memcpy function of the newlib C library. Advanced virtual prototyping for cyber-physical systems using RISC-V (Sci China Inf Sci 2022, §6.1)

[4] Concolic testing suffers from the path-explosion problem and may be susceptible to scalability issues due to complex symbolic constraints, motivating complementary methods such as coverage-guided fuzzing. Advanced virtual prototyping for cyber-physical systems using RISC-V (Sci China Inf Sci 2022, §6.1–6.2)

[5] Abstraction-driven concolic testing iteratively combines concolic testing with model checking; when concolic testing fails to cover some test goals, the model checker refines its abstraction to prove more paths infeasible, reducing the search space. Abstraction-driven Concolic Testing (arXiv 1511.02615v2)

[6] An implementation built on CREST and CPAchecker improved branch coverage compared to standalone CREST from 48% to 63% in the best case and from 66% to 71% on average on SV-COMP benchmarks. Abstraction-driven Concolic Testing (arXiv 1511.02615v2)

[7] A previous approach to concolic testing in logic programming was not sound because it only dealt with positive constraints (by means of substitutions); a subsequent framework lifts concolic testing to CLP, where both positive and negative constraints can be represented naturally, yielding a sound and potentially more efficient technique. Concolic Testing in CLP (arXiv 2008.00421v3)

[8] In RTL hardware verification, concolic testing is described as a semi-formal method that generates effective test sequences by analyzing the control-flow graph of RTL designs and uses coverage scores to guide subsequent sequence generation. DeepVerifier: Learning to Update Test Sequences for Coverage-Guided Verification (ACM TODAES 2026)

[9] Lyu and Mishra utilized concolic testing to activate assertions by regarding assertions as branches and searching through the branch statement tree with heuristics to obtain a path and generate test stimuli that cover the targeted branches. LLM4DV: Using Large Language Models for Hardware Test Stimuli Generation