1. 11

Abstract: “Predictive models are fundamental to engineering reliable software systems. However, designing conservative, computable approximations for the behavior of programs (static analyses) remains a difficult and error-prone process for modern high-level programming languages. What analysis designers need is a principled method for navigating the gap between semantics and analytic models: analysis designers need a method that tames the interaction of complex languages features such as higher-order functions, recursion, exceptions, continuations, objects and dynamic allocation.

We contribute a systematic approach to program analysis that yields novel and transparently sound static analyses. Our approach relies on existing derivational techniques to transform high-level language semantics into low-level deterministic state-transition systems (with potentially infinite state spaces). We then perform a series of simple machine refactorings to obtain a sound, computable approximation, which takes the form of a non-deterministic state-transition systems with finite state spaces. The approach scales up uniformly to enable program analysis of realistic language features, including higher-order functions, tail calls, conditionals, side effects, exceptions, first-class continuations, and even garbage collection.”

  1. 4

    Collapsing Towers of Interpreters, the work of GraalVM/Truffle and PyPy.

    Exciting times! CToI deserves its own lobsters post.

    1. 3

      Submit it next week then.

    2. 4

      A moderately ambitious talk by Matthew Might is Winning the war on error and it references this very paper.

      1. 2

        Didn’t get around to watching this until today. Noted that he advises to read https://www.ccs.neu.edu/home/dvanhorn/pubs/vanhorn-might-jfp12.pdf instead of the linked version

      2. 3

        This is one of the most powerful tools around for making extremely precise compiler analysis passes without much effort.

        1. 4

          Are you saying you like the ideas in the paper or have previously seen/used the technique? I found it through my semi-blind searches. I don’t know if it had uptake.

          1. 4

            Well I think this idea has been deeloped further into the monadic aam approach. It hasn’t been applied in practice yet to my knowledge, except maybe for a java analysis.