package coq-prosa

  1. Overview
  2. No Docs
A Foundation for Formally Proven Schedulability Analysis

Install

Dune Dependency

prosa.mpi-sws.org Edit opam file Versions (2)

Authors

  1. F
    Felipe Cerqueira
  2. B
    Björn Brandenburg
  3. M
    Maxime Lesourd
  4. S
    Sergey Bozhko
  5. X
    Xiaojie Guo
  6. S
    Sophie Quinton
  7. M
    Marco Perronet

Maintainers

  1. P
    Pierre Roux <pierre.roux@onera.fr>

Sources

prosa_v04.zip
sha256=5e11497895528700672e6881da6819962a34702efe1713f61309c50f0f853957

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 logpath:prosa

Published: 24 Feb 2020

Dependencies (2)

  1. coq-mathcomp-ssreflect >= "1.9" & < "1.10~"
  2. coq >= "8.9" & < "8.11~"

Dev Dependencies

None

Used by

None

Conflicts

None