Abstracting abstract machines: A systematic approach to higher-order program analysis

Academic Article

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, firstclass continuations, and even garbage collection. © 2011 ACM.
  • Authors

    Digital Object Identifier (doi)

    Author List

  • Van Horn D; Might M
  • Start Page

  • 101
  • End Page

  • 109
  • Volume

  • 54
  • Issue

  • 9