PV0 ⊧ Prosa: formally PROven Schedulability Analysisa repository of definitions and proofs for real-time schedulability analysis

a repository of models/definitions and analyses/proofs for real-time schedulability analysis, built and verified with Coq

Application domain/field

Schedulability

Type of tool

Zoo

Internals

Coq

Comments

Could fit on PV0 but contains fully verified specs