Counterexample-Driven Debugging¶

Why It Matters¶

Abstract failures are hard to fix: "the system sometimes deadlocks" is not actionable. Concrete counterexamples make failures tangible: "when thread A holds lock L1 and waits for L2 while thread B holds L2 and waits for L1" shows exactly what's wrong. Counterexamples are also test cases - if you fix the bug, the counterexample should no longer trigger it.

The Key Move¶

When something fails (a test, an assertion, a specification check), don't just note "it failed." Capture the exact sequence of inputs, states, and actions that led to failure. Minimize this sequence - remove steps that aren't necessary to trigger the bug. Use this minimal counterexample to understand root cause, test fixes, and build regression tests.

Classic Application¶

Model checker output. When model checking finds a safety violation, it produces a counterexample trace: a sequence of states from initial to violating. This trace shows exactly how to reach the bad state. Engineers use it to understand the bug, often discovering the root cause is much earlier in the trace than the violation.

Surprising Application¶

Failed predictions. When your prediction is wrong, don't just update your belief - extract the counterexample. What specific evidence contradicted your model? What was the minimal scenario that caused failure? This makes learning concrete: not "I was wrong about politics" but "I predicted X because I assumed Y, but Z happened, showing Y is false in condition W."

Failure Modes¶

Non-minimal counterexamples - including irrelevant details that obscure the actual cause. Fixating on the symptom (where the error appeared) rather than the root cause (what caused it). Overfitting the fix to the specific counterexample without addressing the class of failures. Treating counterexamples as one-off bugs rather than systematic failures.

Go Deeper¶

Clarke et al., Model Checking, Chapter 3; Zeller, Why Programs Fail, Chapter 5