Backward Tracing

Concept

Backward tracing is a diagnostic reasoning and analysis technique that starts from a known effect, symptom, or specification and works backward to identify the causes, inputs, or faults that produce it. In hardware reliability verification, backward tracing uses formal model checking to enumerate all faults (such as Single Event Upsets) that violate a defined correct-behavior property, rather than injecting individual faults forward and observing their effects. In software debugging research, backward tracing is one of two complementary reasoning modes developers alternate between while constructing a mental model of a buggy system.

First seen 7/10/2026

Last seen 7/10/2026

Evidence 3 chunks

Wiki v1

WIKI

Backward Tracing

Definition

Backward tracing is an analysis strategy in which the investigator begins from a specified effect, behavior, or symptom and reasons or searches backward toward the causes, inputs, or faults that could produce it. It is the conceptual inverse of forward tracing, in which causes (e.g., specific fault injections) are chosen first and the resulting effects are observed.

READ FULL ARTICLE →

NEIGHBORHOOD

No graph connections found for this entity yet. It may appear in future ingestion runs.

explore full graph →

RELATIONSHIPS

2 connections

Using Formal Verification to Evaluate Single Event Upsets in a RISC-V Core ← uses 100% 2e

The paper proposes backward tracing to identify and categorize faults by their effects.

Forward Tracing compares with → 95% 1e

Backward tracing identifies faults from effects, while forward tracing injects and monitors.

LINKED ENTITIES

2 links

Using Formal Verification to Evaluate Single Event Upsets in a RISC-V Core USES Extracted graph relationship

Forward Tracing COMPARES_WITH Extracted graph relationship

CITATIONS

7 sources

7 citations — click to expand

[1] Backward tracing is a formal-verification strategy that starts from a specified correct behavior (expressed as formal properties such as SystemVerilog Assertions) and uses model checking to identify all faults that may violate those properties, rather than injecting specific faults and monitoring their responses. Using Formal Verification to Evaluate Single Event Upsets in a RISC-V Core

[2] Forward tracing (e.g., simulation-based fault injection) explores at most one fault and one path per run, while backward tracing via model checking leaves fault-control signals unconstrained and can explore all paths and the whole fault list at once, identifying multiple faults violating different assertions in a single run. Using Formal Verification to Evaluate Single Event Upsets in a RISC-V Core

[3] The backward-tracing method partitions SEU fault effects into four groups — no effect, Silent Data Corruption (SDC), Crash, and Hang — and develops three corresponding groups of formal properties (strobe/architectural SDC properties, crash properties, and hang properties). Using Formal Verification to Evaluate Single Event Upsets in a RISC-V Core

[4] Application of backward tracing to the RISC-V Ibex Core found that misaligned instructions can amplify fault effects, that some bits are more vulnerable than others, that most bits are vulnerable to SDC, and that the second pipeline stage is more vulnerable to SDC than the first. Using Formal Verification to Evaluate Single Event Upsets in a RISC-V Core

[5] The hardware backward-tracing approach is, in principle, general to other RISC-V processors because the SVA properties can be adapted via signal remapping. Using Formal Verification to Evaluate Single Event Upsets in a RISC-V Core

[6] In professional software debugging, developers alternate between navigation and execution strategies and employ forward and backward tracing modes of reasoning while iteratively updating a mental model of the system. A Grounded Theory of Debugging in Professional Software Engineering Practice

[7] In the ConCovUp concurrency-testing framework, LLM-driven backward tracing deduces concrete inputs that satisfy complex path constraints and iteratively refines them via dynamic execution feedback, raising average SMAP coverage from 36.6% to 68.1% over a general agent baseline on nine real-world C/C++ libraries. ConCovUp: Effective Agent-Based Test Driver Generation for Concurrency Testing