Merge requests · RT-PROOFS

Equivalence of EDF Predicates

rt-proofs!113 · created Sep 09, 2020 by LailaElbeheiry
- Merged
- 23
updated Mar 11, 2021
Additivity theory

rt-proofs!127 · created Feb 23, 2021 by Ghost User
- Merged
- 38
updated Mar 08, 2021
Compile with Coq 8.13 and mathcomp 1.12

rt-proofs!131 · created Mar 08, 2021 by Pierre Roux
- Merged
- 2
updated Mar 08, 2021
Define completion sequences

rt-proofs!121 · created Sep 28, 2020 by Pierre Roux
Definition Discussion
- Merged
- 12
- Approved
updated Mar 08, 2021
Added `bigcat` over sequences

rt-proofs!125 · created Feb 19, 2021 by Ghost User
- Merged
- 34
updated Mar 01, 2021
Add a few lemmas to sum

rt-proofs!128 · created Feb 25, 2021 by Sergey Bozhko
- Merged
- 10
updated Mar 01, 2021
Ssrlia refactoring

rt-proofs!124 · created Jan 29, 2021 by Ghost User
- Merged
updated Jan 29, 2021
Sum refactoring

rt-proofs!123 · created Dec 14, 2020 by Ghost User
- Merged
- 3
- 1
updated Jan 02, 2021
optimize names for run-to-completion threshold functions

rt-proofs!120 · created Sep 25, 2020 by Sergey Bozhko
- Merged
- 2
updated Dec 11, 2020
Minor documentation changes about tactics.

rt-proofs!122 · created Nov 17, 2020 by Martin Constantino–Bodin
- Merged
- 1
updated Dec 11, 2020
generalize definition of busy interval

rt-proofs!119 · created Sep 25, 2020 by Sergey Bozhko
- Merged
- 1
updated Sep 25, 2020
Add [arrives_in] to [sequential_tasks] definition

rt-proofs!118 · created Sep 23, 2020 by Sergey Bozhko
- Merged
- 2
updated Sep 24, 2020
Max arrivals to rbf

rt-proofs!111 · created Sep 08, 2020 by Ghost User
- Merged
- 30
updated Sep 22, 2020
proof-state recorder tweaks and fixes

rt-proofs!117 · created Sep 22, 2020 by Björn Brandenburg
- Merged
updated Sep 22, 2020
Add Request Bound Functions

rt-proofs!106 · created Aug 27, 2020 by Pierre Roux
- Merged
- 11
- Approved
updated Sep 10, 2020
Prove optimality of work-conserving EDF schedules

rt-proofs!109 · created Sep 01, 2020 by LailaElbeheiry
- Merged
- 7
- Approved
updated Sep 09, 2020
fix minor warning

rt-proofs!112 · created Sep 09, 2020 by Björn Brandenburg
updated Sep 09, 2020
Define a "shifted job costs" function and prove its validity.

rt-proofs!110 · created Sep 02, 2020 by Ghost User
- Merged
- 1
- Approved
updated Sep 09, 2020
Two small lemmas

rt-proofs!107 · created Aug 27, 2020 by Pierre Roux
- Merged
- 4
updated Aug 28, 2020
Support mathcomp 1.11.0 and Coq 8.12

rt-proofs!104 · created Aug 06, 2020 by Björn Brandenburg
- Merged
- 3
updated Aug 28, 2020