package coq-prosa
A Foundation for Formally Proven Schedulability Analysis
Install
Dune Dependency
Authors
Maintainers
Sources
rt-proofs-v0.5.tar.gz
sha256=49b246784fb32137079c3aebbade1dc648d7a7cc705bdc91789ee3e144ea8279
Description
Prosa is a repository of definitions and proofs for real-time schedulability analysis built with Coq. Prosa’s distinguishing characteristic is that Prosa prioritizes readability over all other concerns to ensure that specifications remain accessible to readers without a background in formal proofs. (A background in real-time scheduling is assumed.)
Tags
keyword:prosa keyword:real-time keyword:schedulability analysis keyword:response-time analysis logpath:prosaPublished: 08 Nov 2022
Dependencies (4)
-
coq-coqeal
>= "1.1.0" -
coq-mathcomp-zify
>= "1.2.0" -
coq-mathcomp-ssreflect
(>= "1.12" & < "1.16~") -
coq
(>= "8.13" & < "8.17~")
Dev Dependencies
None
Used by
None
Conflicts
None
On This Page