2 They said, SMT solver used in dynamic symbolic execution tool is in fact a model checker, that checks property violations or path constraints. Symbolic execution found 30 % bugs, which other program analyses missed.

Sergey Vartanov, 2007–2020