Near-Concrete Program Interpretation

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.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.


Ah nuts!

Thanks for the link. I've fixed the post with the 2007 paper.

Time to become a

Time to become a contributing editor, methinks...