Software Diagnostics and Observability Institute

PDF: https://www.dumpanalysis.org/files/Using_Lean_in_Pattern-Oriented_Diagno...

When we recognize an analysis pattern in a memory dump or software trace, we also make a diagnostic statement. Which relationships support it? What assumptions does its interpretation require? What happens when the evidence changes?

In this article, we explore Lean as a formal companion to Pattern-Oriented Diagnostics. After a short introduction, we construct and check examples involving Wait Chain, Deadlock, and Missing Message. We examine a dependency path, introduce a timeout into a restricted deadlock model, and identify the capture condition needed to interpret an absent message as an absent event.

The examples include both checked proofs and deliberately rejected claims. We can reproduce them, modify their evidence and assumptions, and observe which conclusions remain justified. Along the way, we distinguish recorded structures from reconstructed behavior and consider how formal companions can extend our analysis pattern languages and diagnostic narratives.

The accompanying examples are available in our LeanPOD repository.