Abstract

Dynamic symbolic execution has gathered a lot of attention in recent years as a key ingredient in areas including software engineering, programming languages, cybersecurity, and computer systems.

While dynamic symbolic execution is primarily a testing and analysis technique, it has also been used in program verification. In this talk, I will discuss its opportunities and limitations in a verification context, and also argue for the need of testing as a complement to verification.

Keynote @ 16th International Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2024).