Near-Concrete Program Interpretation
Goal: Develop a highly precise and powerful program analysis applicable across a wide range of higher-order programming paradigms.
Publications
Paritosh Shroff, Scott Smith and Christian Skalka, Near-Concrete Program Interpretation [Technical Report (formal details in Appendix)] [Implementation] draft.
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.
Last modified: Mon Jul 24 12:11:08 EDT 2006