Merge requests · RT-PROOFS

Valid arrival sequence

rt-proofs!309 · created Jun 13, 2023 by Pierre Roux
- Merged
updated Jun 13, 2023
Cleanup

rt-proofs!308 · created Jun 13, 2023 by Pierre Roux
- Merged
- 1
updated Jun 13, 2023
Make abstract quiet time bool

rt-proofs!306 · created Jun 06, 2023 by Sergey Bozhko
- Merged
- 1
updated Jun 12, 2023
Silence a non-uniform coercion warning

rt-proofs!307 · created Jun 09, 2023 by Pierre Roux
- Merged
- 1
updated Jun 12, 2023
clean up priority-related facts

rt-proofs!304 · created Apr 26, 2023 by Björn Brandenburg
- Merged
- 15
- Approved
updated Apr 28, 2023
clean up some FIFO facts

rt-proofs!303 · created Apr 25, 2023 by Björn Brandenburg
- Merged
- 1
- Approved
updated Apr 25, 2023
add hints to avoid busy-window destruct'ing

rt-proofs!302 · created Apr 20, 2023 by Björn Brandenburg
- Merged
- 6
- Approved
updated Apr 20, 2023
silence some warnings

rt-proofs!300 · created Apr 19, 2023 by Björn Brandenburg
- Merged
- 2
updated Apr 20, 2023
RTA for ELF scheduling policy

rt-proofs!298 · created Apr 13, 2023 by Meenal Gupta
- Merged
- 219
- Approved
updated Apr 19, 2023
Integrate rt_eauto into done (hence by and //)

rt-proofs!299 · created Apr 19, 2023 by Pierre Roux
- Merged
- 3
updated Apr 19, 2023
update guidelines

rt-proofs!289 · created Apr 06, 2023 by Björn Brandenburg
- Merged
- 4
updated Apr 14, 2023
generalize preemption_time and priority-model compliance to any processor model

rt-proofs!276 · created Mar 27, 2023 by Björn Brandenburg
- Merged
- 15
- Approved
updated Apr 14, 2023
Amend FP bounded_nps to use generalised JLFP PI lemmas

rt-proofs!297 · created Apr 11, 2023 by Meenal Gupta
- Merged
updated Apr 11, 2023
change POET's task notation

rt-proofs!294 · created Apr 06, 2023 by Björn Brandenburg
- Merged
- 4
updated Apr 11, 2023
weaken one assumption

rt-proofs!295 · created Apr 10, 2023 by Kimaya Bedarkar
updated Apr 10, 2023
Add some helper lemmas

rt-proofs!291 · created Apr 06, 2023 by Kimaya Bedarkar
- Merged
- 47
updated Apr 10, 2023
CI: switch to custom mathcomp image

rt-proofs!293 · created Apr 06, 2023 by Björn Brandenburg
updated Apr 06, 2023
using the general JLFP pi lemmas in edf result

rt-proofs!290 · created Apr 06, 2023 by Meenal Gupta
- Merged
- 5
- Approved
updated Apr 06, 2023
generalised Priority Inversion Lemmas for JLFP policies.

rt-proofs!285 · created Apr 04, 2023 by Meenal Gupta
- Merged
- 18
updated Apr 06, 2023
adding helper lemmas for workload partitioning for ELF

rt-proofs!288 · created Apr 05, 2023 by Meenal Gupta
- Merged
- 18
- Approved
updated Apr 06, 2023