Merge requests · RT-PROOFS

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
RTAs for three preemption models of RS FP

rt-proofs!369 · created Apr 22, 2024 by Sergey Bozhko
- Merged
- 53
updated Apr 29, 2024
Prove RTA for RS FIFO

rt-proofs!366 · created Apr 04, 2024 by Sergey Bozhko
- Merged
- 103
- Approved
updated Apr 18, 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
Misc. Cleanups

rt-proofs!367 · created Apr 12, 2024 by Björn Brandenburg
- Merged
- Approved
updated Apr 12, 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
port to MathComp 2

rt-proofs!358 · created Jan 25, 2024 by Björn Brandenburg
- Merged
- 13
updated Feb 25, 2024
Generalize one lemma

rt-proofs!327 · created Oct 19, 2023 by Kimaya Bedarkar
- Merged
- 121
- Approved
updated Feb 14, 2024
add some lemmas about RBFs

rt-proofs!360 · created Feb 08, 2024 by Kimaya Bedarkar
- Merged
- 22
- Approved
updated Feb 13, 2024
add some guidelines

rt-proofs!333 · created Nov 09, 2023 by Kimaya Bedarkar
- Merged
- 1
updated Feb 09, 2024
add some lemmas about workload

rt-proofs!361 · created Feb 08, 2024 by Kimaya Bedarkar
- Merged
- 6
- Approved
updated Feb 09, 2024
prove RS-RTA for fully preemptive FP

rt-proofs!320 · created Jul 13, 2023 by Sergey Bozhko
- Merged
- 79
updated Feb 07, 2024
small refactor of arrivals lemmas

rt-proofs!353 · created Jan 22, 2024 by Kimaya Bedarkar
- Merged
- 19
- Approved
updated Feb 06, 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
Prove a few auxiliary lemmas

rt-proofs!356 · created Jan 24, 2024 by Sergey Bozhko
- Merged
- 3
updated Jan 24, 2024
Prove that job's max lower-priority non-preemptive segment is bounded

rt-proofs!355 · created Jan 23, 2024 by Sergey Bozhko
- Merged
- 4
updated Jan 24, 2024
Prove that abstract search space is a subset of RS-FP search space

rt-proofs!352 · created Jan 22, 2024 by Sergey Bozhko
- Merged
- 16
updated Jan 23, 2024
Refactor assumptions in a lemma about RBF

rt-proofs!354 · created Jan 23, 2024 by Sergey Bozhko
- Merged
- 1
updated Jan 23, 2024
De-duplicate [blocking_bound]

rt-proofs!350 · created Jan 19, 2024 by Sergey Bozhko
- Merged
- 9
updated Jan 22, 2024
Prove lemmas about restricted supply proc. and change SBF def

rt-proofs!349 · created Jan 19, 2024 by Sergey Bozhko
- Merged
- 3
updated Jan 19, 2024