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 Maida
  8. K
    Kimaya Bedarkar

Maintainers

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

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

Published: 08 Nov 2022

Dependencies (4)

  1. coq-coqeal >= "1.1.0"
  2. coq-mathcomp-zify >= "1.2.0"
  3. coq-mathcomp-ssreflect (>= "1.12" & < "1.16~")
  4. coq (>= "8.13" & < "8.17~")

Dev Dependencies

None

Used by

None

Conflicts

None