Publications

Publications related to Prosa in reverse-chronological order:

Lars Willemsen, Mario Günzel, Björn Brandenburg, Georg von der Brüggen, Ching-Chi Lin, and Jian-Jia Chen,, “Transfer Schedulability in Periodic Real-Time Systems”, presented at the ACM International Conference on Embedded Software (EMSOFT 2025), published in the ACM Transactions on Embedded Computing Systems, Volume 24, Issue 5s, pp. 1–25, October 2025.
Kimaya Bedarkar, Laila Elbeheiry, Michael Sammler, Lennard Gäher, Björn Brandenburg, Derek Dreyer, and Deepak Garg, “RefinedProsa: Connecting Response-Time Analysis with C Verification for Interrupt-Free Schedulers”, presented at the 46th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2025), published in the Proceedings of the ACM on Programming Languages, Volume 9, Issue PLDI, pp. 73–97, June 2025.
Sergey Bozhko, Filip Marković, Georg von der Brüggen, and Björn Brandenburg, “What Really is pWCET? A Rigorous Axiomatic Proposal”, Proceedings of the 44th IEEE Real-Time Systems Symposium (RTSS 2023), pp. 13–26, December 2023.
Pascal Fradet, Xiaojie Guo, and Sophie Quinton, “CertiCAN certifying CAN analyses and their results”, Real-Time Systems, Volume 59, Issue 2, pp. 160–198, March 2023.
Kimaya Bedarkar, Mariam Vardishvili, Sergey Bozhko, Marco Maida, and Björn Brandenburg, “From Intuition to Coq: A Case Study in Verified Response-Time Analysis of FIFO Scheduling”, Proceedings of the 43rd IEEE Real-Time Systems Symposium (RTSS 2022), pp. 197–210, December 2022.
Marco Maida, Sergey Bozhko, and Björn Brandenburg, “Foundational Response-Time Analysis as Explainable Evidence of Timeliness”, Proceedings of the 34th Euromicro Conference on Real-Time Systems (ECRTS 2022), pp. 19:1–19:25, July 2022. Outstanding Paper Award.
Pierre Roux, Sophie Quinton, and Marc Boyer, “A Formal Link Between Response Time Analysis and Network Calculus”, Proceedings of the 34th Euromicro Conference on Real-Time Systems (ECRTS 2022), pp. 5:1–5:22, July 2022.
Marco Maida, Sergey Bozhko, and Björn Brandenburg, “Work-in-Progress: Automatically Generated Response-Time Proofs as Evidence of Timeliness”, Proceedings of the 42nd IEEE Real-Time Systems Symposium — Brief Presentations Track (RTSS-BP 2021), pp. 512–516, December 2021.
Xiaojie Guo, Lionel Rieg, and Paolo Torrini, “A Generic Approach for the Certified Schedulability Analysis of Software Systems”, Proceedings of the 27th IEEE International Conference on Embedded and Real-Time Computing Systems and Applications (RTCSA 2021), pp. 83–92, August 2021.
Sergey Bozhko and Björn Brandenburg, “Abstract Response-Time Analysis: A Formal Foundation for the Busy-Window Principle”, Proceedings of the 32nd Euromicro Conference on Real-Time Systems (ECRTS 2020), pp. 22:1–22:24, July 2020. Outstanding Paper Award.
Xiaojie Guo, Maxime Lesourd, Mengqi Liu, Lionel Rieg, Zhong Shao, “Integrating Formal Schedulability Analysis into a Verified OS Kernel”, Computer Aided Verification, 2019
Pascal Fradet, Xiaojie Guo, Jean-François Monin, Sophie Quinton, “CertiCAN: A Tool for the Coq Certification of CAN Analysis Results”, Proceedings of the 25th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS 2019), April 2019.
Pascal Fradet, Maxime Lesourd, Jean-François Monin, and Sophie Quinton, “A Generic Coq Proof of Typical Worst-Case Analysis”, Proceedings of the 39th IEEE Real-Time Systems Symposium (RTSS 2018), December 2018.
Pascal Fradet, Xiaojie Guo, Jean-François Monin, and Sophie Quinton, “A Generalized Digraph Model for Expressing Dependencies”, Proceedings of the 26th International Conference on Real-Time Networks and Systems (RTNS 2018), October 2018.
Felipe Cerqueira, Geoffrey Nelissen, and Björn Brandenburg, “On Strong and Weak Sustainability, with an Application to Self-Suspending Real-Time Tasks”, Proceedings of the 30th Euromicro Conference on Real-Time Systems (ECRTS 2018), pp. 26:1–26:21, July 2018. Outstanding Paper Award.
Antonin Riffard, Felipe Cerqueira, and Björn Brandenburg, “Towards Synchronization in Prosa”, Proceedings of the ECRTS 2018 Work-in-Progress Session, pp. 7–9, July 2018.
Arpan Gujarati, Felipe Cerqueira, Björn Brandenburg, and Geoffrey Nelissen, “Correspondence article: A correction of the reduction-based schedulability analysis for APA scheduling“, Real-Time Systems, August 2018.
Xiaojie Guo, Sophie Quinton, Pascal Fradet, and Jean-François Monin, “Work In Progress: Toward a Coq-certified Tool for the Schedulability Analysis of Tasks with Offsets”, RTSS 2017 Work-in-Progress Track, December 2017.
Felipe Cerqueira, Felix Stutz, and Björn Brandenburg, “Prosa: A Case for Readable Mechanized Schedulability Analysis”, Proceedings of the 28th Euromicro Conference on Real-Time Systems (ECRTS 2016), pp. 273–284, July 2016. Best Paper Award.