Skip to content

Latest commit

 

History

History
 
 

Symbolic Execution for Humans

Folders and files

NameName
Last commit message
Last commit date

parent directory

..
 
 

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