Merge requests · RT-PROOFS

Properly deprecate ltn_leq_trans

rt-proofs!200 · created Mar 16, 2022 by Pierre Roux
- Merged
- 1
updated Mar 16, 2022
Simplify proof of conversion_preserves_equivalence

rt-proofs!193 · created Feb 25, 2022 by Pierre Roux
- Merged
- 12
- 1
updated Mar 14, 2022
improve readability of `service_on` in ideal uniprocessor model

rt-proofs!199 · created Mar 11, 2022 by Björn Brandenburg
updated Mar 11, 2022
GEL policy

rt-proofs!197 · created Mar 08, 2022 by Ghost User
- Merged
- 15
updated Mar 11, 2022
Update the `esy` package

rt-proofs!196 · created Mar 07, 2022 by Martin Constantino–Bodin
- Merged
updated Mar 11, 2022
document #86 in the style guidelines

rt-proofs!194 · created Mar 03, 2022 by Björn Brandenburg
updated Mar 04, 2022
Replace ssrlia with mczify

rt-proofs!186 · created Feb 14, 2022 by Pierre Roux
- Merged
- 9
updated Mar 03, 2022
Put State inside ProcessorState

rt-proofs!192 · created Feb 25, 2022 by Pierre Roux
- Merged
- 2
updated Feb 25, 2022
Deprecate ltn leq trans

rt-proofs!189 · created Feb 18, 2022 by Pierre Roux
- Merged
- 2
updated Feb 21, 2022
Move lemma [early_hep_job_is_scheduled] to separate file

rt-proofs!156 · created Oct 06, 2021 by Sergey Bozhko
- Merged
- 2
updated Feb 18, 2022
Update to latest Coq 8.15 and mathcomp 1.14

rt-proofs!184 · created Feb 09, 2022 by Björn Brandenburg
- Merged
- 12
updated Feb 17, 2022
service_on instead of service_in in the class ProcessorState

rt-proofs!126 · created Feb 22, 2021 by Martin Constantino–Bodin
- Merged
- 28
- Approved
updated Feb 17, 2022
Change [job_task j = tsk] to [job_of_task tsk j]

rt-proofs!179 · created Dec 13, 2021 by Sergey Bozhko
- Merged
- 5
updated Feb 16, 2022
Require external libraries first

rt-proofs!187 · created Feb 14, 2022 by Pierre Roux
- Merged
- 2
- Approved
updated Feb 15, 2022
Add RTA for FIFO based on the aRTA

rt-proofs!182 · created Jan 05, 2022 by Kimaya Bedarkar
- Merged
- 33
- Approved
updated Feb 09, 2022
New helper lemma about RBF

rt-proofs!183 · created Jan 28, 2022 by Kimaya Bedarkar
- Merged
updated Jan 31, 2022
Introduce eta-max vector

rt-proofs!161 · created Oct 08, 2021 by Sergey Bozhko
- Merged
- 15
updated Jan 13, 2022
Bounded tardiness definition

rt-proofs!180 · created Dec 14, 2021 by Ghost User
- Merged
- 5
- Approved
updated Dec 15, 2021
Fix a comment in job.v

rt-proofs!178 · created Dec 07, 2021 by Sophie Quinton
- Merged
- 1
updated Dec 08, 2021
Changes in RBF lemmas

rt-proofs!177 · created Nov 25, 2021 by Kimaya Bedarkar
- Merged
- 4
- Approved
updated Nov 29, 2021