validation - 符号执行的应用

Question

符号执行的应用是什么？只symbolic execution生成? path condition如何使用符号执行来验证contract？

Answer 1

符号执行最著名的用法是测试输入生成。例如，KLEE是一个使用符号执行为 C 程序生成测试输入的工具。

另一个应用是断言检查。如果通过合同您的意思是前置条件和后置条件，那么是的，符号执行也可以用于该目的。