Replication Dataset for Provably Relevant HAL Interface Requirements for Embedded Systems

This archive contains the replication dataset for the REFSQ 2026 paper Provably Relevant HAL Interface Requirements for Embedded Systems. The replication dataset includes the experimental results from the preliminary case study, specifically the source code of the application programs with annotated HAL functions, as well as the verification results produced by the software model checker Ultimate Automizer. The files are organized into directories for source code, verification results, and the configuration files and scripts needed to rerun the experiments. A README.md file in the archive provides detailed instructions for viewing the source code of the application programs, accessing the verification results, and rerunning Ultimate Automizer to reproduce the verification outcomes. The dataset requires CMake (>= 3.10), GNU C Compiler, GNU Make, and Ultimate Automizer (0.3.0) for successful replication.