SoK: A Modularized Framework for Symbolic Execution and Application for Usable Tool Design

Summary

Symbolic Execution (SE) is an important and foundational software testing technique that has grown and evolved in its use over the decades. Prior work has cataloged this evolution, but this paper seeks to identify opportunities to go beyond existing designs and push forward the boundaries of its use by breaking down critical components of SE and outlining current approaches to each. To this end, we performed a systemization of 225 SE papers from the last 15 years to identify common design patterns and use cases. From this review, we distill five distinct modules of the SE architecture and discuss current implementations for each. This division of SE into modules can highlight opportunities for future improvements to SE by helping research focus on individual components. To demonstrate the modules’ utility, we use the modules to identify changes for each module necessary to improve SE usability building on a second systemization of 66 papers containing insights about tooling usability.