Semantic Logical Relations for Timed Message-Passing Protocols

Explore a 19-minute conference talk from POPL 2025 that presents a novel approach to verifying timed message-passing protocols in heterogeneous systems. Learn how researchers from Carnegie Mellon University and University at Buffalo developed semantic logical relations to verify compliance with timed protocols, particularly crucial for Internet of Things (IoT) and real-time systems with inherent timing constraints. The presentation introduces a semantic approach that enables verification without requiring systems to be implemented in a common language, allowing for both systematic verification of well-typed applications and per-instance verification of specific hardware devices. Discover how the team implemented a refinement type system in Rust with SMT solver integration to check timing constraints, and see their approach demonstrated through a smart home air quality monitoring case study. The talk includes references to available artifacts that have been functionally evaluated, with links to the full article and supplementary materials.