Merge requests · RT-PROOFS

Draft: Add RS ELF RTA for fully-preemptive preemption model

rt-proofs!375 · created Dec 23, 2024 by Athul Raj Kollareth
updated Dec 25, 2024
CI: replace `make validate` with `Print Assumptions`

rt-proofs!374 · created Dec 16, 2024 by Björn Brandenburg
updated Dec 16, 2024
CI: bump Coq to 8.20 and mathcomp to 2.3.0

rt-proofs!373 · created Dec 16, 2024 by Björn Brandenburg
updated Dec 16, 2024
Add definition for Demand Bound Function

rt-proofs!372 · created Oct 26, 2024 by Athul Raj Kollareth
- Merged
- 194
- 1
- Approved
updated Nov 29, 2024
Draft: Formalize pRTA from "Critical Instant for Probabilistic Timing Guarantees: Refuted and Revisited"

probsa!1 · created Sep 06, 2024 by Sergey Bozhko
- 2
updated Nov 25, 2024
define periodic resource model

rt-proofs!371 · created May 02, 2024 by Sergey Bozhko
- 16
updated Dec 16, 2024
prove RTAs for two preemption models of RS EDF

rt-proofs!370 · created May 01, 2024 by Sergey Bozhko
- Merged
- 3
- Approved
updated Dec 13, 2024
RTAs for three preemption models of RS FP

rt-proofs!369 · created Apr 22, 2024 by Sergey Bozhko
- Merged
- 53
updated Apr 29, 2024
Remove classic work conservation hypothesis from busy interval bound proof

rt-proofs!368 · created Apr 17, 2024 by Kimaya Bedarkar
- Merged
- 15
updated Dec 17, 2024
Misc. Cleanups

rt-proofs!367 · created Apr 12, 2024 by Björn Brandenburg
- Merged
- Approved
updated Apr 12, 2024
Prove RTA for RS FIFO

rt-proofs!366 · created Apr 04, 2024 by Sergey Bozhko
- Merged
- 103
- Approved
updated Apr 18, 2024
make typeclasses into records

rt-proofs!365 · created Mar 14, 2024 by Kimaya Bedarkar
- 8
updated Dec 10, 2024
Remove work conservation dependence from the priority inversion file

rt-proofs!364 · created Mar 13, 2024 by Kimaya Bedarkar
- Merged
- 51
updated Apr 12, 2024
Prove RTA for RS-FP-EDF and RS-NP-EDF

rt-proofs!363 · created Feb 21, 2024 by Sergey Bozhko
- Merged
- 116
updated Apr 17, 2024
add file for non seq rta

rt-proofs!362 · created Feb 14, 2024 by Kimaya Bedarkar
- 73
updated Dec 18, 2024
add some lemmas about workload

rt-proofs!361 · created Feb 08, 2024 by Kimaya Bedarkar
- Merged
- 6
- Approved
updated Feb 09, 2024
add some lemmas about RBFs

rt-proofs!360 · created Feb 08, 2024 by Kimaya Bedarkar
- Merged
- 22
- Approved
updated Feb 13, 2024
remove proof-term from JobReady type-class

rt-proofs!359 · created Feb 06, 2024 by Sergey Bozhko
- 8
updated Feb 13, 2024
port to MathComp 2

rt-proofs!358 · created Jan 25, 2024 by Björn Brandenburg
- Merged
- 13
updated Feb 25, 2024
prove that busy intervals are bounded for RS-FP

rt-proofs!357 · created Jan 24, 2024 by Sergey Bozhko
- Merged
- 24
updated Jan 25, 2024