Advances in Comparing Solvers for Constrained Horn Clauses and Report on CHC-COMP 2024 and 2025 -- Artifact Archive

Advances in Comparing Solvers for Constrained Horn Clauses and Report on CHC-COMP 2024 and 2025 -- Artifact Archive This archive contains the data and scripts accompanying the "Advances in Comparing Solvers for Constrained Horn Clauses and Report on CHC-COMP 2024 and 2025" paper. Contents Folder Description results/ BenchExec result XML files for all participating solvers and all categories chc-comp25-benchmarks/ The benchmark set used in the competition chc-comp25-scripts/ Competition infrastructure scripts (BenchExec configuration, model validation, plotting) data-analysis-scripts/ Python scripts used to produce the statistics and figures in the paper Note on participant tool archives The binary archives of the participant tools are not included in this artifact due to licensing concerns. The competition was run using BenchExec tool archives; please contact the respective tool authors for their binaries. Reproducing the paper's plots and tables The figures and LaTeX table fragments in the paper are generated from the data in results/ and chc-comp25-benchmarks/ using the scripts in data-analysis-scripts/. Requirements Python 3.8+ Python packages: matplotlib, pyyaml Install dependencies with: pip install matplotlib pyyaml Step 1 — Majority-vote relabeling (optional) If you want to recompute the benchmark ground-truth verdicts using a majority vote over all solver results, run: python3 data-analysis-scripts/majority-vote-relabel.py \ chc-comp25-benchmarks \ results \ --output-dir output This updates the .yml task definition files and the expectedVerdict attributes in the result XMLs. The results already included in this archive have been produced with this relabeling applied. Step 2 — Parse model-validation results To generate the model-validation summary table used in the paper: python3 data-analysis-scripts/parse-model-validation.py \ results \ output Output is written to output/model-validation.csv and a corresponding LaTeX table fragment. Step 3 — Generate competition statistics, tables, and cactus plots python3 data-analysis-scripts/generate-statistics.py \ chc-comp25-benchmarks \ results \ output This produces: Per-category and overall solver statistics (correct, wrong, timeout, unknown, …) LaTeX table fragments ready for inclusion in the paper Cactus plots (SVG) per category and one overall plot All output is written to the output/ directory (created automatically if it does not exist).