Guiding dynamic symbolic execution toward unverified program executions
Maria Christakis, Peter Müller, Valentin Wüstholz · 2016
Most techniques to detect program errors, such as testing, code reviews, and static program analysis, do not fully verify all possible executions of a program. They leave executions unverified when they do not check certain properties, fail to verify properties, or check properties under certain unsound assumptions such as the absence of arithmetic overflow.