Artifact for Safe Temperature Regulation: Formally Verified and Real-World Validated

This is the reproducibility package for Safe Temperature Regulation: Formally Verified and Real-World Validated accepted at iFM 2025. This case study presents a deductively verified generic controller for safe temperature regulation using a lumped capacitance model of heat transfer. The proof of safety was carried out in differential dynamic logic (dL) and formalized in KeYmaera X. Moreover, the correctness of the controller was validated on a real incubator. This reproducibility package contains two artifacts. First, the formal proof of correctness in KeYmaera X syntax with a Docker image to run KeYmaera X to verify the proof's correctness. Second, the experimental data of the real-world experiment that was collected and interpreted in the paper, together with a visualization script for convenience.