Symbolic Execution and Program Testing
approach originally outlined here.
1 EFFIGY—symbolic executor for PL/I. This work is for program analysis without formal specification. They assume, the program is correct on the sample if it produses correct results on it.
Two extreme alternatives: program testing and program proving (e.g. formal analysis). Proving doesn't need program execution. So, is it always static? SE is between these two alternatives.
Sergey Vartanov, 2007–2020