Experimental Results (CBMC, CBMC-refine, and PBEAR)

The script files contain information for each target program (obj (P1), elev (P2), brobot (P3), and sv (SV-COMP)) along with the corresponding execution options:<i>origin</i>: Execute only CBMC without function summary replacement.<i>refine</i>: Execute only CBMC-refine without function summary replacement.<i>pbear</i>: Execute PBEAR.<i>no_alarm</i>: Execute PBEAR without symbolic alarm filtering (PBEAR^base).<i>without_cov</i>: Execute PBEAR without considering output coverage (PBEAR^-cov).In Results directory,filter/: the details of (concrete) symbolic alarm filtering process.synth/: the details of PBE-based FS refinement.target.c: the abstracted program.cbmc_result.txt: the result of CBMC with target.c.result.txt: the overall result of each property falsification. We have used different terminology than what was used in the paper. For example, we used 'FS' as 'stub' and 'symbolic alarm filtering' as 'true alarm filtering,' etc.Another important point is that, due to our mistake, the input/output examples of the "<i>check</i>" function in the "<i>seq-mthreaded"</i> category were missed. As a result, new input/output examples were created, leading to differences in the experimental results of PBEAR compared to what was initially documented in the paper. Nevertheless, PBEAR still successfully solved 2 out of 3 benchmarks in the category, while PBEAR^-cov failed to solve any.