Sound Termination and Non-Termination Analysis of C Programs with Bit-Precise Bounded Semantics and Advanced Constructs

This artifact accompanies the FSE 2026 paper “Sound Termination and Non-Termination Analysis of C Programs with Bit-Precise Bounded Semantics and Advanced Constructs.” It archives the Athena framework and the materials required to reproduce the experiments reported in the paper. Athena is an end-to-end framework for sound termination and non-termination analysis of C programs, with support for finite-width, bit-precise integer semantics and advanced constructs including pointers, arrays, structures, and bitwise operations. The artifact includes the Athena implementation, installation and execution scripts, benchmark programs under Benchmarks/, archived evaluation outputs under EvaluationResults/, reproduced outputs generated under ReproducedResults/, and the standard artifact documentation (README, REQUIREMENTS, INSTALL, STATUS, LICENSE, and a copy of the accepted paper). The provided scripts support both demo and full experimental runs, enabling reproduction of the evaluation reported in the paper on the 2024 Termination Competition (TermCOMP) benchmarks and on 117 real-world benchmarks featuring 445 non-termination bugs, after excluding benchmarks that rely on undefined behavior.