VeriRT: An End-To-End Verification Framework for Real-Time Distributed Systems

Watch this 19-minute conference talk from POPL 2025 where researchers from Seoul National University and Yale University present VeriRT, an end-to-end formal verification framework designed to bridge the gap between high-level abstract timed specifications and low-level implementations for real-time distributed systems. Learn about the theoretical foundation for constructing formal timed operational semantics by integrating conventional operational semantics with low-level timing assumptions. Discover how the framework leverages CompCert's correctness proofs to guarantee the correctness of assembly implementations for safety-critical real-time distributed systems. The presentation includes two case studies on realistic real-time systems, with all results formalized in Coq. The talk features work by Yoonseung Kim, Sung-Hwan Lee, Yonghyun Kim, and Chung-Kil Hur, with supplementary materials available that have earned "Artifacts Available" and "Artifacts Evaluated — Reusable" badges.