符号执行使用符号化的值作为输入来模拟程序的执行,其不同于常规的"数据执行"之处在于得到的变量值是输入符号和常量的表达式.由于符号的值不确定,所以在遇到执行分支（这里的分支指的是由于符号的值不确定而导致程序执行步骤有不同的选择方向而产生的分支）的时候必须作出某种假设.
路径是一组按照某种顺序执行的语句.PC(Path Constraints)是输入符号的约束条件的集合,是各分支的假设的综合.符号执行当且仅当其PC得到满足的时候才会沿着一条路径执行.因此需要定理证明器来解决PC问题.处理模块调用的方法有两种：函数摘要[参考文献5]和宏展开.函数摘要通过把函数替换为其摘要来执行内部过程分析,每个函数只符号执行一次,而宏展开则进入函数体内部,例如在每个调用该函数的地方都把宏（的全部内容）展开.函数摘要方法是（比宏展开）更加灵活的内部过程分析技术.