Partial Verification Results
Valentin Tobias WÃ ⁄ stholz · Repository for Publications and Research Data (ETH Zurich) · 2015
In recent years, program analysis tools have been increasingly applied to real-world software to prevent defects as early as possible.Examples of such tools include both static analyzers and automatic test case generation tools.While the la er traditionally underapproximate the possible program executions to find errors, the former traditionally consider additional program executions that are not actually possible in the analyzed program.This makes it possible to efficiently analyze programs with a large or infinite number of program executions and to prove the correctness of the analyzed program in case the analysis over-approximates the possible program executions (i.e., is sound).As a consequence, static analyzers may report spurious errors that do not reveal real defects in the analyzed program.