Switch branches/tags
Nothing to show
Find file History
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Type Name Latest commit message Commit time
Failed to load latest commit information.


Symbolic Execution for Humans

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