Artifact for FM 2026 Paper: "Array-Carrying Symbolic Execution for Function Contract Generation"

Artifact for the FM 2026 paper: "Array-Carrying Symbolic Execution for Function Contract Generation" This artifact contains the replication package for the tools ACSLGen and AutoDeduct, as presented in the paper. Artifact Contents: Prebuilt Docker images for both tools (acslgen.tar.gz, autodeduct.tar.gz). Source code and scripts for ACSLGen and AutoDeduct. Benchmarks (FM2026 set and openHiTLS targets). Scripts to reproduce the claims and main results. System Requirements (Recommended): OS: Linux x86_64 with Docker Engine (>= 20.10). CPU: 8+ cores. RAM: 16+ GB (32 GB recommended). Disk: 60+ GB free space. Quick Start (Smoke Test): Load the prebuilt images: docker load -i acslgen.tar.gz docker load -i autodeduct.tar.gz Run ACSLGen smoke test (approx. 1 min): docker run --rm -it -w /app/benchmark-FM2026 acslgen:latest bash -lc 'SUITES_OVERRIDE=basic BASIC_FUNCS_OVERRIDE=BN_Create SKIP_BUILD=1 bash experiment_adapted.sh' Run AutoDeduct smoke test (approx. 1 min): docker run --rm -it -w /home/dev/repos autodeduct:latest bash -lc 'mkdir -p /tmp/ae_smoke && cp benchmark/fib_46_benchmark/01.c /tmp/ae_smoke && ./benchmark_infer_verify.sh /tmp/ae_smoke' Evaluation Claims: Reproduces end-to-end automatic ACSL generation and WP verification on FM2026 benchmarks. Generates consolidated reports for comparison of success/failure distributions. Important Notes: The exact numeric counts may vary slightly due to solver timeouts and hardware differences. For AutoDeduct, some "verified" results in the raw output may correspond to trivial contracts (requires true; ensures true;), which are counted as failures in the paper (see README Section 8). For detailed instructions, please refer to the README.md file included in the package.