Paper artifact

Process Equivalence Checking as Abstract Interpretation

This paper ventures to flesh out that equivalence checking constitutes a form of backward-complete abstract interpretation on pairs of processes.

This site publishes the current paper artifact together with generated API documentation for the Lean autoformalization.

Paper PDF Download the Quarto-rendered paper as a PDF artifact. Lean Theory Docs Browse the published API documentation for the Lean development.
Austronauts meme: Program equivalence checking is just abstract interpretation? -- Alwasys has been.

Benjamin Bisping, 2026. Licensed under CC BY 4.0.