symbolic-execution icon indicating copy to clipboard operation
symbolic-execution copied to clipboard

Challenge: symbolic execution with higher-order values

Open dvanhorn opened this issue 8 years ago • 0 comments

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

dvanhorn avatar Jun 10 '17 15:06 dvanhorn