我正在考虑使用符号执行来测试用特定语言(例如 java)编写的程序的健壮性。我读过一些介绍符号执行基本概念的论文。但我不清楚如何开始。
例如,如何从具体输入生成约束条件?
那么任何人都可以就符号执行的实现基础知识给我一些建议吗?此外,concolic execution(concrete +symbolic) 呢?
最佳答案
也许你可以从 Symbolic PathFinder http://babelfish.arc.nasa.gov/trac/jpf/wiki/projects/jpf-symbc 开始