Symbolic execution is a program analysis technique which offers a powerful theoretical foundation for automated testing and verification of programs. Compared to traditional software testing, which verifies a single possible program execution, symbolic execution reasons about numerous executions simultaneously through automatic identification of program semantics. This systematic approach yields high analysis coverage and is useful in applications such as automated test generation, bug discovery, and debugging. Symbolic execution complements fuzz testing, and the two can be paired to find deeper and more complex bugs than could be found by either technique in isolation. Yet, despite existing in academic research for over 40 years and being used in high-profile events such as the DARPA Cyber Grand Challenge, symbolic execution remains relatively unknown and unused in software testing workflows.
Mark Mossberg offers a practical introduction to symbolic execution, exploring cutting-edge research in automated software testing, along with its strengths, weaknesses, and applications. Mark uses Manticore, a simple, usable, symbolic execution tool, to bridge theory and practice with concrete examples. You’ll walk away better prepared to make informed decisions about how to test your software.
Presented at
Authored by
- Mark Mossberg