Merge requests · RT-PROOFS / PROSA - Formally Proven Schedulability Analysis

convert epsilon to notation to avoid unfolding it

!332 · created Nov 09, 2023 by Kimaya Bedarkar
- Merged
- 1
updated Nov 10, 2023
bump mathcomp version to 1.18

!331 · created Nov 06, 2023 by Björn Brandenburg
updated Nov 08, 2023
Add guideline about strict subproofs

!330 · created Nov 02, 2023 by Kimaya Bedarkar
- Merged
updated Nov 02, 2023
Silence some warnings

!329 · created Nov 02, 2023 by Kimaya Bedarkar
- Merged
- 21
- Approved
updated Nov 09, 2023
simplify one proof

!328 · created Oct 19, 2023 by Kimaya Bedarkar
- Merged
- 1
updated Nov 02, 2023
Generalize one lemma

!327 · created Oct 19, 2023 by Kimaya Bedarkar
- Merged
- 121
- Approved
updated Feb 14, 2024
remove [sequential_tasks] assumption in one proof

!326 · created Oct 12, 2023 by Sergey Bozhko
- Merged
- 1
updated Oct 12, 2023
Import ssreflect only once

!325 · created Oct 11, 2023 by Sergey Bozhko
- Merged
- 1
updated Oct 13, 2023
Draft: refactor cumul task interference

!324 · created Oct 09, 2023 by Kimaya Bedarkar
- Closed
- 4
updated Oct 12, 2023
CI: bump Coq version to 8.18

!323 · created Sep 22, 2023 by Björn Brandenburg
updated Sep 22, 2023
update definition of SBF

!322 · created Sep 15, 2023 by Sergey Bozhko
- Merged
- 13
updated Nov 22, 2023
Draft: Elf preemption instantiations

!321 · created Jul 17, 2023 by Meenal Gupta
- 43
updated Mar 23, 2024
prove RS-RTA for fully preemptive FP

!320 · created Jul 13, 2023 by Sergey Bozhko
- Merged
- 79
updated Feb 07, 2024
Add sequential restricted-supply aRTA

!319 · created Jul 05, 2023 by Sergey Bozhko
- Merged
- 98
updated Jan 04, 2024
Elf bounded nps

!318 · created Jul 01, 2023 by Meenal Gupta
- Merged
- 47
- Approved
updated Jul 05, 2023
Remove ideal assumption from aRTA-seq and generalize proof [task_IBF -> job_IBF]

!317 · created Jun 29, 2023 by Sergey Bozhko
- Merged
- 49
updated Jul 07, 2023
utility lemmas and cleanups needed for a later ELF MR

!316 · created Jun 29, 2023 by Björn Brandenburg
- Merged
- 5
- Approved
updated Jun 29, 2023
Removal of Ideal Uniproc. Model from Busy Interval Reasoning

!315 · created Jun 28, 2023 by Björn Brandenburg
- Merged
- 26
- 1
- Approved
updated Jul 04, 2023
Add "conditional" interference to remove duplication

!314 · created Jun 20, 2023 by Sergey Bozhko
- Merged
- 105
updated Jul 05, 2023
Draft: PCP-RTA

!313 · created Jun 19, 2023 by Sergey Bozhko
- 7
- 1
updated Jan 16, 2024