{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,12]],"date-time":"2026-05-12T01:20:36Z","timestamp":1778548836958,"version":"3.51.4"},"reference-count":48,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,1,7]]},"abstract":"<jats:p>Safety-critical systems are often designed as real-time distributed systems. Despite the need for strong guarantees of safety and reliability in these systems, applying formal verification methods to real-time distributed systems at the implementation level has faced significant technical challenges.<\/jats:p>\n                  <jats:p>\n                    In this paper, we present\n                    <jats:sc>VeriRT<\/jats:sc>\n                    , an end-to-end formal verification framework that closes the formal gap between high-level abstract timed specifications and low-level implementations for real-time distributed systems.Within the framework, we establish a theoretical foundation for constructing formal timed operational semantics by integrating conventional operational semantics and low-level timing assumptions, along with principles for reasoning about their timed behaviors against abstract specifications. We leverage CompCert\u2019s correctness proofs to guarantee the correctness of the assembly implementation of real-time distributed systems. We provide two case studies on realistic real-time systems. All the results are formalized in Coq.\n                  <\/jats:p>","DOI":"10.1145\/3704897","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"1812-1839","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["VeriRT: An End-to-End Verification Framework for Real-Time Distributed Systems"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5294-1046","authenticated-orcid":false,"given":"Yoonseung","family":"Kim","sequence":"first","affiliation":[{"name":"Seoul National University, Seoul, South Korea"},{"name":"Yale University, New Haven, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0783-7033","authenticated-orcid":false,"given":"Sung-Hwan","family":"Lee","sequence":"additional","affiliation":[{"name":"Seoul National University, Seoul, South Korea"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-9834-5352","authenticated-orcid":false,"given":"Yonghyun","family":"Kim","sequence":"additional","affiliation":[{"name":"Seoul National University, Seoul, South Korea"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1656-0913","authenticated-orcid":false,"given":"Chung-Kil","family":"Hur","sequence":"additional","affiliation":[{"name":"Seoul National University, Seoul, South Korea"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1109\/IEEESTD.2020.9120376"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s42045-020-00032-z"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/EMSOFT.2013.6658583"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2009.50"},{"key":"e_1_3_2_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_3_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0020949"},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1109\/EMRTS.2003.1212753"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1109\/ECRTS.2016.28"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/PCCC.2017.8280498"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1109\/26.47845"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","unstructured":"Michelle Cotton and Leo Vegoda. 2010. Special Use IPv4 Addresses. RFC 5735. https:\/\/doi.org\/10.17487\/RFC5735 10.17487\/RFC5735","DOI":"10.17487\/RFC5735"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01784024"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2406336.2406340"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837650"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.net.2016.10.009"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485474"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523444"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.2001.955072"},{"key":"e_1_3_2_21_1","unstructured":"Aeronautical Radio Inc. 2005. ARINC Specification 664: Aircraft Data Network Part 7 - Avionics Full Duplex Switched Ethernet (AFDX) Network."},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSYST.2014.2322503"},{"key":"e_1_3_2_23_1","doi-asserted-by":"publisher","unstructured":"Yoonseung Kim Sung-Hwan Lee Yonghyun Kim and Chung-Kil Hur. 2024. Artif act for POPL 2025 - VeriRT: An End-To-End Verification Framework for Real-Time Distributed Systems. https:\/\/doi.org\/10.5281\/zenodo.13937956 10.5281\/zenodo.13937956","DOI":"10.5281\/zenodo.13937956"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385980"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","unstructured":"Xavier Leroy. 2009a. Formal verification of a realistic compiler. Commun. ACM 52 7 (July 2009) 107\u2013115. https:\/\/doi.org\/10.1145\/1538788.1538814 10.1145\/1538788.1538814","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","unstructured":"Xavier Leroy. 2009b. A formally verified compiler back-end. Journal of Automated Reasoning 43 4 (2009) 363\u2013446. https:\/\/doi.org\/10.1007\/s10817-009-9155-4 10.1007\/s10817-009-9155-4","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837622"},{"key":"e_1_3_2_29_1","doi-asserted-by":"publisher","DOI":"10.1109\/ISORC.2011.38"},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/361227.361234"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECRTS.2022.19"},{"key":"e_1_3_2_32_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSAMOS.2010.5642071"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3166227.3166230"},{"key":"e_1_3_2_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCOM.1976.1093424"},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2012.05.040"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","unstructured":"D. Mills. 1992. RFC1305: Network Time Protocol (Version 3) Specification Implementation. https:\/\/doi.org\/10.17487\/RFC1305 10.17487\/RFC1305","DOI":"10.17487\/RFC1305"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693017_26"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-007-9001-5"},{"key":"e_1_3_2_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2008.09.022"},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/AERO.2012.6187151"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/DDECS.2017.7934571"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158116"},{"key":"e_1_3_2_43_1","unstructured":"Lui Sha Abdullah Al-Nayeem Mu Sun Jose Meseguer and Peter C Olveczky. 2009. PALS: Physically asynchronous logically synchronous systems. Technical Report."},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/WCSP.2011.6096958"},{"key":"e_1_3_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371091"},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571232"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290372"},{"key":"e_1_3_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2813885.2737958"},{"key":"e_1_3_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2854065.2854081"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704897","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704897","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:15:55Z","timestamp":1770200155000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704897"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":48,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704897"],"URL":"https:\/\/doi.org\/10.1145\/3704897","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}