A relational framework for bounded program verification

[摘要] (cont.) Unlike testing, many static analyses are not equipped with coverage metrics to detect which program behaviors the analysis failed to exercise. Our framework, in contrast, includes such a metric. When no counterexamples are found, the metric can report how thoroughly the code was covered. This information can, in turn, help the user change the bound on the analysis or strengthen the specification to make subsequent analyses more comprehensive.

[发布机构] Massachusetts Institute of Technology