README.md

Prosa: Formally Proven Schedulability Analysis

This repository contains the main Coq specification & proof development of the Prosa open-source project, which was launched in 2016.

From 2018–201, Prosa was further developed in the context of the RT-Proofs research project (funded jointly by ANR and DFG, projects ANR-17-CE25-0016 and DFG-391919384, respectively).

Prosa continues to be maintained and developed by the MPI-SWS Real-Time Systems group and contributors. Patches and merge requests are very welcome!

Documentation

Up-to-date documentation for all branches of the main Prosa repository is available on the Prosa homepage:

• https://prosa.mpi-sws.org/branches

Publications

Please see the list of publications on the Prosa project's homepage.