Interactive Visualization of Abstract Machines for Static Analysis 📊

We present an approach for interactively visualizing static analyses built using the abstracting abstract machines (AAM)
methodology—a process that yields a static program analysis by abstract interpretation of an abstract machine. The resulting
analysis is a state graph of all possible machine states—with paths through this graph encoding possible executions of the
program—combined with a model of the heap. To understand or audit the results of such an analysis (e.g., for debugging or
improving the analysis) can become a laborious process of stepping from state to state, building an intuition for each, while
considering valid executions that are missing and spurious executions that are included. Finding states relevant to some
program property, on its own, can involve writing a custom predicate to match such states at the REPL.
In this paper, we explore an approach to concisely visualizing AAM-based analyses of Scheme programs by decomposing
the analysis into its functional components and displaying nested graphs for inter- and intra-procedural control flow. We
allow interactive visualization in that the user can focus on specific functions or lines of code to discover if they’re reachable,
in what contexts, atop what stacks, and with what values bound to variables in scope, in terms of states in an abstract abstract
machine.

Presenter: Kyle Headly
Authors: Kyle Headly, Clark Ren
Paper: https://thomas.gilray.org/pdf/viz-aam.pdf
Presented at the Scheme workshop 2019: https://icfp19.sigplan.org/home/scheme-2019, part of ICFP'19: icfp19.sigplan.org