1. 5

From the Abstract:

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.

There’s also an accompanying visualization system here: https://analysisviz.gilray.net/

  1. 2

    Beautiful typesetting, though I’m not 100% convinced on the line number thing.

    On topic, is AAM or such static analyses used in practice or is it just an academic thing? It seems like an interesting field.

    1. 1

      seriously, completely agreed about the visual presentation.

      wrt AAMs and the like, we definitely use them at work a bit, but it’s not in any of the production tools we currently ship; our research tools & ideas definitely pass in that direction, tho over time those will be pushed down more towards our production tooling.