Prosa is an open-source project by and for real-time systems researchers. It is currently being maintained by the MPI-SWS real-time systems group.
The project was initially launched by Felipe Cerqueira and Björn Brandenburg of the real-time systems group at the Max Planck Institute for Software Systems (MPI-SWS) in Kaiserlautern, Germany.
From 2018 until 2021, it was further developed by several groups as part of the French-German RT-Proofs project.
The goals of the Prosa project exceed the scope of what any single group can sustain in the long term. We therefore envision Prosa to transition into a true community effort and actively seek collaborators at all levels of expertise.
The Prosa team is generally happy to help if you have any questions or are stuck with getting started in using Coq for research on real-time systems.
To contact us, please post your questions in the #prosa-helpdesk
channel in the Real-Time Systems Discord server.
You may use the following invitation link to join the Real-Time Systems Discord server:
Any and all contributions are welcome, including questions and suggestions, critiques and constructive criticism, patches, alternative formalizations, new directions, etc.
Please contact us in the #prosa-helpdesk
channel or file an issue on GitLab if you are interested in contributing but unsure where to begin or how to submit patches.
If you have experience with formal methods and/or real-time systems and would be interested in working on Prosa, please contact us by email. Paid internships, funded PhD positions, and post-doc positions are available for qualified candidates.