把一组输入带入程序
符号执行是一种程序分析方法：用代表未知输入的符号代替某些具体数值，在执行指令时同时维护程序位置、变量的符号表达式和路径条件。它不是单纯化简一个代数式，而是跟随程序的控制流，记录哪些输入会使执行走到当前位置。一次符号执行状态可以代表许多具体运行。
设一个使用数学整数的简化程序先计算 y=x+1，再依次检查 x>0 和 y<4。两次都进入真分支时，路径条件为 x>0 且 x+1<4，所以整数输入只能是 1 或 2。若另一条候选路径同时要求 x>0 与 x<0，条件就相互矛盾。真实语言还需按实际整数位宽、溢出规则和内存行为建模，不能直接把这个数学整数例子当作任意 C 程序的语义。
从路径条件到测试输入
执行器把条件交给约束求解器。可满足时，模型给出一组具体输入，可以用来生成到达目标分支的测试；不可满足时，可排除这个模型下的对应路径。Z3 明确区分可满足、不可满足和未知三种结果：未知表示它未能作出判定，绝不能当成路径不可行，也不能当成程序安全。
动态符号执行常把具体运行与符号分析结合。微软 IntelliTest 先执行选定输入，跟踪经过的条件，再利用求解器寻找尚未覆盖路径的新输入，如此反复。这里的测试生成依靠路径条件，不等同于随机试数；但输入能否构造、环境如何模拟，都会限制可探索的行为。
路径数量与合并代价
分支不断分叉会造成路径爆炸。若 n 次二选一都相互独立且可行，就可能形成 2 的 n 次方种组合；循环还会增加不同迭代次数的路径。设置展开上限或时间预算可以限制工作量，却不能证明边界以外没有错误。
状态合并试图在合适的程序位置，把不同路径的信息精确保存在一个状态中。例如两条路分别令 z=2 和 z=9，合并后必须保留“按原分支条件选择 2 或 9”的表达式，而不能随便取一个值。这样减少了状态数，却引入更复杂的条件表达式和求解查询。库兹涅佐夫等人的研究因此选择性地合并状态，并兼顾搜索顺序；合并越多，并不保证分析越快。
参考：[2]
环境模型与结论边界
程序还会读取文件、调用库函数或访问操作系统。KLEE 的研究实现同时使用真实环境交互和符号环境模型，并把生成的输入放回原生程序中重放。若直接把外部调用的参数具体化，就只观察到该次交互；若改用模型，则必须说明模型允许哪些文件、返回值或失败情况。模型不完整会留下盲区，模型失真也会影响结果。
因此，找到可重现的反例与证明整个程序正确是不同成果。在语义准确、约束求解可靠的前提下，符号推理可以证明特定路径上的性质；覆盖全部相关行为还需要额外的完整性条件。只执行了部分路径、限制了循环次数，或留下未知查询时，即使所有生成测试都通过，也不能升级为不受这些边界限制的全程序证明。