Challenge: symbolic execution with higher-order values

[dvanhorn]

One challenge the article omits is that of handling behavioral values such as first-class functions. This is addressed in the following papers:

• Higher-Order Symbolic Execution via Contracts. Sam Tobin-Hochstadt and David Van Horn.
  The ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'12), Tuscon, Arizona, October 2012. http://dl.acm.org/citation.cfm?id=2384655

• Soft Contract Verification. With Phuc C. Nguyen, Sam Tobin-Hochstadt, and David Van Horn.
  The ACM SIGPLAN International Conference on Functional Programming (ICFP'14), Gothenburg, Sweden, September 2014. http://dl.acm.org/citation.cfm?id=2628156

• Relatively Complete Counterexamples for Higher-Order Programs. Phuc C. Nguyen and David Van Horn. The 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'15), Portland, Oregon, June, 2015. https://dl.acm.org/citation.cfm?id=2737971