{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:01:51Z","timestamp":1767927711866,"version":"3.49.0"},"reference-count":43,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","funder":[{"name":"ERC","award":["803111"],"award-info":[{"award-number":["803111"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,6,10]]},"abstract":"<jats:p>There has been a recent upsurge of interest in formal, machine-checked verification of timing guarantees for C implementations of real-time system schedulers. However, prior work has only considered tick-based schedulers, which enjoy a clearly defined notion of time: the time \"quantum\". In this work, we present a new approach to real-time systems verification for interrupt-free schedulers, which are commonly used in deeply embedded and resource-constrained systems but which do not enjoy a natural notion of periodic time. Our approach builds on and connects two recently developed Rocq-based systems\u2014RefinedC (for foundational C verification) and Prosa (for verified response-time analysis)\u2014adapting the former to reason about timed traces and the latter to reason about overheads. We apply the resulting system, which we call RefinedProsa, to verify R\u00f6ssl, a simple yet representative, fixed-priority, non-preemptive, interrupt-free scheduler implemented in C.<\/jats:p>","DOI":"10.1145\/3729249","type":"journal-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T16:02:27Z","timestamp":1749830547000},"page":"73-97","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["RefinedProsa: Connecting Response-Time Analysis with C Verification for Interrupt-Free Schedulers"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-1794-6548","authenticated-orcid":false,"given":"Kimaya","family":"Bedarkar","sequence":"first","affiliation":[{"name":"MPI-SWS, Saarbr\u00fccken, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-9514-1360","authenticated-orcid":false,"given":"Laila","family":"Elbeheiry","sequence":"additional","affiliation":[{"name":"MPI-SWS, Saarbr\u00fccken, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4591-743X","authenticated-orcid":false,"given":"Michael","family":"Sammler","sequence":"additional","affiliation":[{"name":"ETH Z\u00fcrich, Z\u00fcrich, Switzerland"},{"name":"ISTA, Klosterneuburg, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2917-375X","authenticated-orcid":false,"given":"Lennard","family":"G\u00e4her","sequence":"additional","affiliation":[{"name":"MPI-SWS, Saarbr\u00fccken, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8254-3815","authenticated-orcid":false,"given":"Bj\u00f6rn","family":"Brandenburg","sequence":"additional","affiliation":[{"name":"MPI-SWS, Kaiserslautern, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3884-6867","authenticated-orcid":false,"given":"Derek","family":"Dreyer","sequence":"additional","affiliation":[{"name":"MPI-SWS, Saarbr\u00fccken, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0888-3093","authenticated-orcid":false,"given":"Deepak","family":"Garg","sequence":"additional","affiliation":[{"name":"MPI-SWS, Saarbr\u00fccken, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_2_2_1_1","unstructured":"AbsInt Angewandte Informatik GmbH. 2024. Qualification Support for AIT. https:\/\/www.absint.com\/ait\/qualification.htm Accessed: 2025-03-22"},{"key":"e_1_2_2_2_1","unstructured":"AbsInt Angewandte Informatik GmbH. 2024. TimeWeaver: Timing Analysis for Task-Interaction Effects. https:\/\/www.absint.com\/timeweaver\/index.htm Accessed: 2025-03-22"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1049\/SEJ.1993.0034"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16256-5_6"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","unstructured":"Kimaya Bedarkar Laila Elbeheiry Michael Sammler Lennard G\u00e4her Bj\u00f6rn Brandenburg Derek Dreyer and Deepak Garg. 2025. Artifact for \"RefinedProsa: Connecting Response-Time Analysis with C Verification for Interrupt-Free Schedulers\". https:\/\/doi.org\/10.5281\/zenodo.15185870 Project webpage: 10.5281\/zenodo.15185870","DOI":"10.5281\/zenodo.15185870"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS55097.2022.00026"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1890028.1890031"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.4230\/OASICS.WCET.2017.5"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECRTS.2021.14"},{"key":"e_1_2_2_10_1","volume-title":"in preparation. Rigorous and General Response-Time Analysis for Uniprocessor Real-Time Systems. Ph. D. Dissertation","author":"Bozhko Sergey","unstructured":"Sergey Bozhko. 2025, in preparation. Rigorous and General Response-Time Analysis for Uniprocessor Real-Time Systems. Ph. D. Dissertation. Saarland University, Germany."},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.4230\/DARTS.6.1.3"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-45410-3"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2012.2188805"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECRTS.2019.6"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECRTS.2018.26"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/ECRTS.2016.28"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/S11241-018-9316-9"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/REAL.2002.1181573"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/S11241-007-9012-7"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2008.66"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/LCN.2004.38"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3273905.3273918"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/S11241-023-09393-2"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2018.00039"},{"key":"e_1_2_2_25_1","volume-title":"12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16)","author":"Gu Ronghui","year":"2016","unstructured":"Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan Newman Wu, Jieung Kim, Vilhelm Sj\u00f6berg, and David Costanzo. 2016. CertiKOS: An extensible architecture for building certified concurrent OS kernels. In 12th USENIX Symposium on Operating Systems Design and Implementation (OSDI 16). 653\u2013669."},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/S11241-018-9315-X"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_28"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTCSA52859.2021.00018"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","unstructured":"Leandro Soares Indrusiak Alan Burns and Borislav Nikolic. 2016. Analysis of buffering effects on hard real-time priority-preemptive wormhole networks. arXiv preprint arXiv:1606.02942 https:\/\/doi.org\/10.48550\/arXiv.1606.02942 10.48550\/arXiv.1606.02942","DOI":"10.48550\/arXiv.1606.02942"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3704897"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","unstructured":"Philip Levis Samuel Madden Joseph Polastre Robert Szewczyk Kamin Whitehouse Alec Woo David Gay Jason Hill Matt Welsh and Eric Brewer. 2005. TinyOS: An operating system for sensor networks. Ambient intelligence 115\u2013148. https:\/\/doi.org\/10.1007\/3-540-27139-2_7 10.1007\/3-540-27139-2_7","DOI":"10.1007\/3-540-27139-2_7"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371088"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563290"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECRTS.2022.19"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.ECRTS.2022.5"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","unstructured":"Michael Sammler Angus Hammond Rodolphe Lepigre Brian Campbell Jean Pichon-Pharabod Derek Dreyer Deepak Garg and Peter Sewell. 2022. Islaris: verification of machine code against authoritative ISA semantics. In PLDI. ACM 825\u2013840. https:\/\/doi.org\/10.1145\/3519939.3523434 10.1145\/3519939.3523434","DOI":"10.1145\/3519939.3523434"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","unstructured":"Michael Sammler Rodolphe Lepigre Robbert Krebbers Kayvan Memarian Derek Dreyer and Deepak Garg. 2021. RefinedC: automating the foundational verification of C code with refined ownership types. In PLDI. ACM 158\u2013174. https:\/\/doi.org\/10.1145\/3453483.3454036 10.1145\/3453483.3454036","DOI":"10.1145\/3453483.3454036"},{"key":"e_1_2_2_39_1","unstructured":"The Digger team. 2024. Digger. https:\/\/github.com\/2xs\/digger"},{"key":"e_1_2_2_40_1","unstructured":"The Prosa team. 2024. Prosa. http:\/\/prosa.mpi-sws.org\/"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2024.3446865"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/RTAS54340.2022.00030"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/S11241-015-9240-1"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729249","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,16]],"date-time":"2025-07-16T06:06:46Z","timestamp":1752646006000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729249"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,10]]},"references-count":43,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2025,6,10]]}},"alternative-id":["10.1145\/3729249"],"URL":"https:\/\/doi.org\/10.1145\/3729249","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,10]]},"assertion":[{"value":"2024-11-15","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}