This artifact is intended for use with https://doi.org/10.5281/zenodo.10928976 (the Artifact Evaluation VM) Hardware Requirements This artifact has no special requirements for running examples and reproducing the analysis results from our experimental raw data. For reproducing the experimental raw data, we recommend a machine with at least 32 GB of memory and at least 10 (virtual) cores. The artifact requires about 50 GB of disk space with experiment reproduction. Smoke Test For details about the below commands and their output, and detailed instructions for use of the artifact, please see the README.html in the Artifact ZIP file. Setup: Run the following command from folder experiments: make install-full This installs all required Ubuntu and Python packages, permanently enables cgroups v1, and installs BenchExec in the VM. Our experiments use BenchExec for reliable benchmark execution and measurement. Expected output: if [ -z "make install-full" ]; then \ export _CALLING_CMD="make bootstrap"; \ fi && \ cd scripts && bash bootstrap.sh Installing deb packages…The sudo password is: artifact [sudo] password for artifact: Please reboot your system to apply the changes. Press enter to exit Enter password 'artifact' when this prompt appears. If you used sudo before, you may not have to enter this. Press enter when you see this output Restart the VM All commands are executed in the terminal. Run the following command (from cpa-daemon-artifact/experiments/cpachecker-grpc): java -jar build/cpadaemon-prod/quarkus-run.jar This runs CPA-Daemon locally, on port 8080. Expected output: __ ____ __ _____ ___ __ ____ ______ --/ __ \/ / / / _ | / _ \/ //_/ / / / __/ -/ /_/ / /_/ / __ |/ , _/ ,>> Creating overview result tables in CSV and HTML Statistics for Response-Time Factor 'Library / Separate JVM' (C-CEGAR): count 3469.000000 mean 75.616010 std 24.538213 min 12.001743 10% 46.007837 25% 55.778796 50% 70.361197 75% 99.300449 99% 129.020641 max 233.229520 dtype: float64 > Stored plot in /home/tacas23/cpa-daemon-artifact/experiments/processed-output/Figure11.pdf To check that experiment reproduction works: Run make clean. This removes our original experiment results from folder results/ (still available at raw-data/) Run CPAchecker experiments (from folder cpa-daemon-artifact/experiments): make response-standalone And cancel the experiments after the first few results. Expected output: cd cpachecker-grpc/cpachecker \ && PYTHONPATH=../../benchexec/:../benchmark-definitions/tool_info ../../benchexec/bin/benchexec --startTime '2023-09-01 10:00:00' -o ../../results/ --read-only-dir / --hidden-dir /home --overlay-dir . --full-access-dir /sys/fs/cgroup --read-only-dir ../../benchexec --read-only-dir ../../sv-benchmarks ../../benchmark-definitions/response-standalone.xml 2023-10-26 20:22:00,573 - INFO - Unable to find pqos_wrapper, please install it for cache allocation and monitoring if your CPU supports Intel RDT (cf. https://gitlab.com/sosy-lab/software/pqos-wrapper). executing run set 'ReachSafety-BelowOneMinute' (1416 files) 20:22:00 bitvector-loops/diamond_2-1.yml false(unreach-call) 7.78 3.77 20:22:04 bitvector-loops/verisec_sendmail_tTflag_arr_one_loop.yml false(unreach-call) 23.25 9.90 20:22:14 bitvector-regression/implicitfloatconversion.yml false(unreach-call) 5.48 2.20 20:22:17 bitvector-regression/implicitunsignedconversion-1.yml false(unreach-call) 6.00 2.25 20:22:19 bitvector-regression/implicitunsignedconversion-2.yml true 6.94 2.76 [.. snip output ..] 7.2 Run experiments for CPA-Daemon with backend 'Native Execution' (from folder `cpa-daemon-artifact/experiments): make response-native And cancel the experiments after the first few results. Expected output: scripts/run-experiments-response.sh native Started quarkus server with PID 984971 Quarkus server PID: 984971 nohup: appending output to 'nohup.out' make[1]: Entering directory '/home/tacas23/cpa-daemon-artifact/experiments' cd cpachecker-grpc \ && PYTHONPATH=../benchexec/:../cpachecker-grpc/connector/tool_info ../benchexec/bin/benchexec --startTime '2023-09-01 10:00:00' -o ../results/ --tool-directory build/toArchive/cpadaemon --network-access --read-only-dir / --hidden-dir /home --overlay-dir . --full-access-dir /sys/fs/cgroup --read-only-dir ../benchexec --read-only-dir ../sv-benchmarks ../benchmark-definitions/response-native.xml 2023-10-26 22:50:32,494 - WARNING - The container configuration disables DNS, host lookups will fail despite --network-access. Consider using --keep-system-config. 2023-10-26 22:50:33,702 - WARNING - The container configuration disables DNS, host lookups will fail despite --network-access. Consider using --keep-system-config. 2023-10-26 22:50:33,905 - INFO - Unable to find pqos_wrapper, please install it for cache allocation and monitoring if your CPU supports Intel RDT (cf. https://gitlab.com/sosy-lab/software/pqos-wrapper). executing run set 'ReachSafety-BelowOneMinute' (1416 files) 22:50:34 bitvector-loops/diamond_2-1.yml false 0.24 0.97 22:50:35 bitvector-loops/verisec_sendmail_tTflag_arr_one_loop.yml false 0.25 4.55 22:50:40 bitvector-regression/implicitfloatconversion.yml false 0.23 0.50 22:50:40 bitvector-regression/implicitunsignedconversion-1.yml false 0.24 0.54 22:50:41 bitvector-regression/implicitunsignedconversion-2.yml true 0.23 0.56 22:50:42 bitvector-regression/integerpromotion-2.yml true 0.24 0.54 22:50:43 bitvector-regression/integerpromotion-3.yml false 0.23 0.49 7.3 Run experiments for C-CEGAR with CPA-Daemon, backend 'Library' (from folder cpa-daemon-artifact/experiments): make ccegar-engine And cancel the experiments after the first few results (we recommand to keep this running for ~1 hour). Expected output: cd cpachecker-grpc \ && cp -rT build/cpadaemon-engine build/quarkus-app PYTHONPATH=benchexec/:benchmark-definitions/tool_info benchexec/bin/benchexec --startTime '2023-09-01 10:00:00' -o results/ --network-access --read-only-dir / --hidden-dir /home --overlay-dir . --full-access-dir /sys/fs/cgroup --read-only-dir benchexec --read-only-dir sv-benchmarks -r c-pred -n c-pred benchmark-definitions/ccegar-engine.xml 2023-10-27 10:06:47,412 - WARNING - The container configuration disables DNS, host lookups will fail despite --network-access. Consider using --keep-system-config. 2023-10-27 10:06:48,015 - WARNING - No files found matching 'ntdrivers-simplified/*.yml'. 2023-10-27 10:06:48,017 - WARNING - No files found matching 'openssl/*.yml'. 2023-10-27 10:06:51,124 - WARNING - No files found matching 'verifythis/duplets.yml'. 2023-10-27 10:06:51,124 - WARNING - No files found matching 'verifythis/elimination_max.yml'. 2023-10-27 10:06:51,125 - WARNING - No files found matching 'verifythis/lcp.yml'. 2023-10-27 10:06:52,949 - WARNING - No files found matching 'recursive-with-pointer/*.yml'. 2023-10-27 10:06:52,949 - WARNING - No files found matching 'verifythis/elimination_max_rec.yml'. 2023-10-27 10:06:52,949 - WARNING - No files found matching 'verifythis/elimination_max_rec_onepoint.yml'. 2023-10-27 10:07:02,420 - WARNING - No files found matching 'ntdrivers-simplified/*.yml'. 2023-10-27 10:07:02,420 - WARNING - No files found matching 'openssl/*.yml'. 2023-10-27 10:07:05,003 - WARNING - No files found matching 'verifythis/duplets.yml'. 2023-10-27 10:07:05,003 - WARNING - No files found matching 'verifythis/elimination_max.yml'. 2023-10-27 10:07:05,003 - WARNING - No files found matching 'verifythis/lcp.yml'. 2023-10-27 10:07:06,604 - WARNING - No files found matching 'recursive-with-pointer/*.yml'. 2023-10-27 10:07:06,604 - WARNING - No files found matching 'verifythis/elimination_max_rec.yml'. 2023-10-27 10:07:06,604 - WARNING - No files found matching 'verifythis/elimination_max_rec_onepoint.yml'. 2023-10-27 10:07:12,456 - WARNING - The container configuration disables DNS, host lookups will fail despite --network-access. Consider using --keep-system-config. 2023-10-27 10:07:12,461 - INFO - Unable to find pqos_wrapper, please install it for cache allocation and monitoring if your CPU supports Intel RDT (cf. https://gitlab.com/sosy-lab/software/pqos-wrapper). Skipping run set 'c-predwit' executing run set 'c-pred' (8872 files) 10:07:12 array-examples/data_structures_set_multi_proc_ground-1.yml 2023-10-27 10:23:44,010 - WARNING - Killing process 3983 due to wall time timeout. TIMEOUT (true) 49.90 991.00 10:23:45 array-examples/data_structures_set_multi_proc_ground-2.yml The "WARNING - No files found matching …" are expected.