Higher-order symbolic execution via contracts
Sam Tobin-Hochstadt, David Van Horn · 2012
We present a new approach to automated reasoning about higher-order programs by extending symbolic execution to use behavioral contracts as symbolic values, thus enabling symbolic approximation of higher-order behavior.