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

simplify one proof

!328 · created Oct 19, 2023 by Kimaya Bedarkar
- Merged
- 1
updated Nov 02, 2023
Import ssreflect only once

!325 · created Oct 11, 2023 by Sergey Bozhko
- Merged
- 1
updated Oct 13, 2023
remove [sequential_tasks] assumption in one proof

!326 · created Oct 12, 2023 by Sergey Bozhko
- Merged
- 1
updated Oct 12, 2023
CI: bump Coq version to 8.18

!323 · created Sep 22, 2023 by Björn Brandenburg
updated Sep 22, 2023
Introduce restricted-supply abstract RTA

!249 · created Oct 26, 2022 by Sergey Bozhko
- Merged
- 29
updated Jul 12, 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
Elf bounded nps

!318 · created Jul 01, 2023 by Meenal Gupta
- Merged
- 47
- Approved
updated Jul 05, 2023
Scheduled jobs in priority inversion

!279 · created Mar 30, 2023 by Pierre Roux
- Merged
- 1
updated Jul 05, 2023
Add "conditional" interference to remove duplication

!314 · created Jun 20, 2023 by Sergey Bozhko
- Merged
- 105
updated Jul 05, 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
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
Factor interference

!305 · created May 31, 2023 by Pierre Roux
- Merged
- 20
updated Jun 27, 2023
Add the notion of Supply Bound Function (SBF)

!312 · created Jun 15, 2023 by Sergey Bozhko
- Merged
- 12
updated Jun 27, 2023
Add notion of supply

!311 · created Jun 15, 2023 by Sergey Bozhko
- Merged
- 65
- Approved
updated Jun 27, 2023
Remove task_interference_received_before_dec

!310 · created Jun 13, 2023 by Pierre Roux
- Merged
- 1
- Approved
updated Jun 13, 2023
Valid arrival sequence

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

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

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

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

!304 · created Apr 26, 2023 by Björn Brandenburg
- Merged
- 15
- Approved
updated Apr 28, 2023