{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:05:57Z","timestamp":1784199957055,"version":"3.55.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>\n                    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 \u201cquantum\u201d. In this work, we present a new approach to real-time systems verification for\n                    <jats:italic toggle=\"yes\">interrupt-free schedulers<\/jats:italic>\n                    , 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\n                    <jats:italic toggle=\"yes\">RefinedProsa<\/jats:italic>\n                    , to verify R\u00f6ssl, a simple yet representative, fixed-priority, non-preemptive, interrupt-free scheduler implemented in C.\n                  <\/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":2,"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":[{"vocabulary":"crossref","role":"author"}]},{"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":[{"vocabulary":"crossref","role":"author"}]},{"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":[{"vocabulary":"crossref","role":"author"}]},{"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":[{"vocabulary":"crossref","role":"author"}]},{"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":[{"vocabulary":"crossref","role":"author"}]},{"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":[{"vocabulary":"crossref","role":"author"}]},{"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":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_3_2_2_2","unstructured":"AbsInt Angewandte Informatik GmbH. 2024. Qualification Support for AIT. https:\/\/www.absint.com\/ait\/qualification.htm Accessed: 2025-03-22."},{"key":"e_1_3_2_3_2","unstructured":"AbsInt Angewandte Informatik GmbH. 2024. TimeWeaver: Timing Analysis for Task-Interaction Effects. www.absint.com\/timeweaver\/index.htm Accessed: 2025-03-22."},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1049\/SEJ.1993.0034"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16256-5_6"},{"key":"e_1_3_2_6_2","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 \u201cRefinedProsa: Connecting Response-Time Analysis with C Verification for Interrupt-Free Schedulers\u201d. doi:10.5281\/zenodo.15185870 Project webpage: https:\/\/plv.mpi-sws.org\/refinedprosa\/.","DOI":"10.5281\/zenodo.15185870"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","unstructured":"Kimaya Bedarkar Mariam Vardishvili Sergey Bozhko Marco Maida and Bj\u00f6rn B.Brandenburg. 2022. From Intuition to Coq: A Case Study in Verified Response-Time Analysis of FIFO Scheduling. In 2022 IEEE Real-Time Systems Symposium (RTSS). 197-210. doi:10.1109\/RTSS55097.2022.00026","DOI":"10.1109\/RTSS55097.2022.00026"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/1890028.1890031"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","unstructured":"Armelle Bonenfant Denis Claraz Marianne De Michiel and Pascal Sotin. 2017. Early WCET Prediction Using Machine Learning. In WCET (OASIcs Vol. 57). Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik 5:1-5:9. doi:10.4230\/OASICS.WCET.2017.5","DOI":"10.4230\/OASICS.WCET.2017.5"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","unstructured":"Marc Boyer Pierre Roux Hugo Daigmorte and David Puechmaille. 2021. A Residual Service Curve of Rate-Latency Server Used by Sporadic Flows Computable in Quadratic Time for Network Calculus. In Proceedings of the 33rd Euromicro Conference on Real-Time Systems (ECRTS). 14:1-14:21. doi:10.4230\/LIPICS.ECRTS.2021.14","DOI":"10.4230\/LIPICS.ECRTS.2021.14"},{"key":"e_1_3_2_11_2","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_3_2_12_2","doi-asserted-by":"publisher","unstructured":"Sergey Bozhko and Bj\u00f6rn B Brandenburg. 2020. Abstract Response-Time Analysis: A Formal Foundation for the Busy-Window Principle. In Proceedings of the 32nd Euromicro Conference on Real-Time Systems (ECRTS). 22:1-22:24. doi:10.4230\/DARTS.6.1.3","DOI":"10.4230\/DARTS.6.1.3"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","unstructured":"Giorgio C Buttazzo. 2011. Hard real-time computing systems: predictable scheduling algorithms and applications. Springer. doi:10.1007\/978-3-031-45410-3","DOI":"10.1007\/978-3-031-45410-3"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1109\/TII.2012.2188805"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","unstructured":"Daniel Casini Tobias Bla\u00df Ingo L\u00fctkebohle and Bj\u00f6rn Brandenburg. 2019. Response-time analysis of ROS 2 processing chains under reservation-based scheduling. In 31st Euromicro Conference on Real-Time Systems. 1-23. doi:10.4230\/LIPICS.ECRTS.2019.6","DOI":"10.4230\/LIPICS.ECRTS.2019.6"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","unstructured":"Felipe Cerqueira Geoffrey Nelissen and Bj\u00f6rn B Brandenburg. 2018. On strong and weak sustainability with an application to self-suspending real-time tasks. In Proceedings of the 30th Euromicro Conference on Real-Time Systems (ECRTS). 26:1-26:21. doi:10.4230\/LIPICS.ECRTS.2018.26","DOI":"10.4230\/LIPICS.ECRTS.2018.26"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","unstructured":"Felipe Cerqueira Felix Stutz and Bj\u00f6rn B Brandenburg. 2016. PROSA: A case for readable mechanized schedulability analysis. In Proceedings of the 28th Euromicro Conference on Real-Time Systems (ECRTS). 273-284. doi:10.1109\/ECRTS.2016.28","DOI":"10.1109\/ECRTS.2016.28"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/S11241-018-9316-9"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","unstructured":"Darren D. Cofer and Murali Rangarajan. 2002. Formal Verification of Overhead Accounting in an Avionics RTOS. In RTSS. IEEE Computer Society 181-190. doi:10.1109\/REAL.2002.1181573","DOI":"10.1109\/REAL.2002.1181573"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/S11241-007-9012-7"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2008.66"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","unstructured":"Adam Dunkels Bjorn Gronvall and Thiemo Voigt. 2004. Contiki-a lightweight and flexible operating system for tiny networked sensors. In 29th annual IEEE international conference on local computer networks. IEEE 455-462. doi:10.1109\/LCN.2004.38","DOI":"10.1109\/LCN.2004.38"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","unstructured":"Pascal Fradet Xiaojie Guo Jean-Fran\u00e7ois Monin and Sophie Quinton. 2018. A generalized digraph model for expressing dependencies. In Proceedings of the 26th International Conference on Real-Time Networks and Systems (RTNS). 72-82. doi:10.1145\/3273905.3273918","DOI":"10.1145\/3273905.3273918"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","unstructured":"Pascal Fradet Xiaojie Guo Jean-Fran\u00e7ois Monin and Sophie Quinton. 2019. CertiCAN: A tool for the Coq certification of CAN analysis results. In Proceedings of the 25th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS). 182-191. doi:10.1007\/S11241-023-09393-2","DOI":"10.1007\/S11241-023-09393-2"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","unstructured":"Pascal Fradet Maxime Lesourd Jean-Fran\u00e7ois Monin and Sophie Quinton. 2018. A Generic Coq Proof of Typical Worst-Case Analysis. In Proceedigns of the 39th IEEE Real-Time Systems Symposium (RTSS). 218-229. doi:10.1109\/RTSS.2018.00039","DOI":"10.1109\/RTSS.2018.00039"},{"key":"e_1_3_2_26_2","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-669."},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","unstructured":"Arpan Gujarati Felipe Cerqueira Bj\u00f6rn B Brandenburg and Geoffrey Nelissen. 2019. Correspondence article: a correction of the reduction-based schedulability analysis for APA scheduling. Real-Time Systems 55 1(2019) 136-143. doi:10.1007\/S11241-018-9315-X","DOI":"10.1007\/S11241-018-9315-X"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_28"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","unstructured":"Xiaojie Guo Lionel Rieg and Paolo Torrini. 2021. A generic approach for the certified schedulability analysis of software systems. In RTCSA. IEEE 83-92. doi:10.1109\/RTCSA52859.2021.00018","DOI":"10.1109\/RTCSA52859.2021.00018"},{"key":"e_1_3_2_30_2","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 (2016). doi:10.48550\/arXiv.1606.02942","DOI":"10.48550\/arXiv.1606.02942"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/3704897"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","unstructured":"Philip Levis Samuel Madden Joseph Polastre Robert Szewczyk Kamin Whitehouse Alec Woo David Gay Jason Hill Matt Welsh Eric Brewer et al. 2005. TinyOS: An operating system for sensor networks. Ambient intelligence (2005) 115-148. doi:10.1007\/3-540-27139-2_7","DOI":"10.1007\/3-540-27139-2_7"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","unstructured":"Mengqi Liu Lionel Rieg Zhong Shao Ronghui Gu David Costanzo Jung-Eun Kim and Man-Ki Yoon. 2019. Virtual timeline: a formal abstraction for verifying preemptive schedulers with temporal isolation. 4 POPL (2019). doi:10.1145\/3371088","DOI":"10.1145\/3371088"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/3563290"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","unstructured":"Marco Maida Sergey Bozhko and Bj\u00f6rn B Brandenburg. 2022. Foundational Response-Time Analysis as Explainable Evidence of Timeliness. In Proceedings of the 34th Euromicro Conference on Real-Time Systems (ECRTS). 19:1-19:25. doi:10.4230\/LIPICS.ECRTS.2022.19","DOI":"10.4230\/LIPICS.ECRTS.2022.19"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","unstructured":"Pierre Roux Sophie Quinton and Marc Boyer. 2022. A Formal Link Between Response Time Analysis and Network Calculus. In Proceedings of the 34th Euromicro Conference on Real-Time Systems (ECRTS). 5:1-5:22. doi:10.4230\/LIPICS.ECRTS.2022.5","DOI":"10.4230\/LIPICS.ECRTS.2022.5"},{"key":"e_1_3_2_38_2","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-840. doi:10.1145\/3519939.3523434","DOI":"10.1145\/3519939.3523434"},{"key":"e_1_3_2_39_2","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-174. doi:10.1145\/3453483.3454036","DOI":"10.1145\/3453483.3454036"},{"key":"e_1_3_2_40_2","unstructured":"The Digger team. 2024. Digger. https:\/\/github.com\/2xs\/digger."},{"key":"e_1_3_2_41_2","unstructured":"The Prosa team. 2024. Prosa. http:\/\/prosa.mpi-sws.org\/."},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","unstructured":"Harun Teper Daniel Kuhse Mario G\u00fcnzel Georg von der Br\u00fcggen Falk Howar and Jian-Jia Chen. 2024. Thread Carefully: Preventing Starvation in the ROS 2 Multi-Threaded Executor. In 2024 International Conference on Embedded Software. doi:10.1109\/TCAD.2024.3446865","DOI":"10.1109\/TCAD.2024.3446865"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","unstructured":"Florian Vanhems Vlad Rusu David Nowak and Gilles Grimaud. 2022. A Formal Correctness Proof for an EDF Scheduler Implementation. In RTAS. IEEE 281-292. doi:10.1109\/RTAS54340.2022.00030","DOI":"10.1109\/RTAS54340.2022.00030"},{"key":"e_1_3_2_44_2","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":[[2026,7,16]],"date-time":"2026-07-16T10:06:51Z","timestamp":1784196411000},"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"}}]}}