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

How to reproduce:Run "<i>mv scripts/compile.sh .</i>" and "<i>mv scripts/run.sh .</i>" commands. Next, run "<i>bash compile.sh</i>". To check if the compilation was successful, also execute "<i>bash run.sh</i>"Perform "<i>mv scripts/synthList.txt .</i>" and "<i>mv scripts/targetList.txt .</i>"Run "<i>bash scripts/test_*.sh</i>" filesThe remaining 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).Note that you can only run "<i>_no_alarm.sh" files after executing "</i><i>*</i><i>_pbear.sh</i>" files (i.e., after synthesizing function summaries). This is because the "<i>no_alarm</i>" option assumes the presence of function summaries sythesized by "<i>pbear.</i>"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.