Higher-order symbolic execution via contracts

We present a new approach to automated reasoning about higher-order programs by extending symbolic execution to use behavioral contracts as symbolic values, enabling sym-bolic approximation of higher-order behavior. Our approach is based on the idea of an abstract reduc-tion semantics that gives an operational semantics to pro-grams with both concrete and symbolic components. Sym-bolic components are approximated by their contract and our semantics gives an operational interpretation of contracts-as-values. The result is a executable semantics that soundly pre-dicts program behavior, including contract failures, for all possible instantiations of symbolic components. We show that our approach scales to an expressive language of con-tracts including arbitrary programs embedded as predicates