Symbolic execution 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