Lambda the Ultimate

Near-Concrete Program Interpretation, By Paritosh Shroff, Scott F. Smith, Christian Skalka:

We develop near-concrete program interpretation (NCI), a higher-order program analysis that achieves high precision via close, yet decidable, simulation of operational (concrete) semantics. NCI models mutable heaps with possibly recursive structure, and achieves flow-, context- and path-sensitivity in a uniform setting. The analysis also extracts a nugget that characterizes the value bindings resulting from program execution; it can be used to statically determine a wide range of non-trivial properties. The technical novelty of the system lies in a prune-rerun technique for approximating recursive functions. To illustrate the generality and usefulness of the system, we show how it can be used to statically enforce temporal program safety, information flow security, and array bounds checking properties.

Very interesting paper that brings sophisticated higher order analysis to abstract interpretation. The paper proves the algorithm is exponential for certain types of programs, akin to ML type inference, and polynomial for first order programs. They have a working implementation in OCaml.