Build Better Defenses
October 29–30, 2017: Training
October 30–November 1, 2017: Tutorials & Conference
New York, NY

Symbolic execution for humans

Mark Mossberg (Trail of Bits)
3:50pm–4:30pm Wednesday, November 1, 2017
Tools and processes
Location: Beekman

Who is this presentation for?

  • Security engineers, software developers, application security directors, researchers, bounty hunters, and CTF players

Prerequisite knowledge

  • General experience with software development, including testing

What you'll learn

  • Explore symbolic execution and understand how to use it in your test infrastructure


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.

Photo of Mark Mossberg

Mark Mossberg

Trail of Bits

Mark Mossberg is a security engineer at Trail of Bits, where he develops and maintains open source binary analysis software.