A System to Generate Test Data and Symbolically Execute Programs

[skyleaworlder]

https://hiper.cis.udel.edu/lp/lib/exe/fetch.php/courses/other-symb-exe-clarke76.pdf

LORI A. CLARKE

from https://github.com/ksluckow/awesome-symbolic-execution.

[skyleaworlder]

1976 年的。

文中提到，一个测试用例生成系统由 “preprocessor”、“symbolic execution”、“constraint simplification” 和 “inequality solver” 四部分组成。但核心部分就是 symbolic execution 与 inequality solver 两处。其中对于符号执行，文中给出的解释是：“在程序执行路径上，将赋值语句看作表达式间的运算，而非看作值的传递；使用表达式来代替一系列变量值的运算过程（无形中构造了一个演化图 evolution graph）”。

Symbolic execution involves assigning expressions instead of values to variables while following a program path.
An expression represents the computation that would have evolved in order to compute each variable's value.
An expression is represented internally as a directed graph.

(图中，假设 B 的值是 X1，C 的值是 X2，D 的值是 X3，5 对应 C1)

[skyleaworlder]

总之，这是一篇 76 年的论文，篇幅很短，并且只提出了一个大概的骨架。我也并没有花特别多时间浏览。