Merge requests · RT-PROOFS

Draft: Initiate a Prosa Tutorial

rt-proofs!134 · created Mar 25, 2021 by Pierre Roux
- Closed
- 4
- 1
updated Feb 22, 2022
Draft: Adding branch with critical sections. Changes to beahviour/schedule.v, new...

rt-proofs!133 · created Mar 22, 2021 by ptorrx
- Closed
- 34
updated Mar 25, 2022
WIP: Pi cleanup

rt-proofs!132 · created Mar 15, 2021 by Sergey Bozhko
- Closed
- 1
updated Mar 15, 2021
Compile with Coq 8.13 and mathcomp 1.12

rt-proofs!131 · created Mar 08, 2021 by Pierre Roux
- Merged
- 2
updated Mar 08, 2021
Switch basic readiness to sequential readiness in [results] folder

rt-proofs!130 · created Mar 05, 2021 by Sergey Bozhko
- Merged
- 62
updated Sep 29, 2021
Add notion of sequential and work bearing readiness

rt-proofs!129 · created Feb 25, 2021 by Sergey Bozhko
- Merged
- 13
updated Jul 27, 2021
Add a few lemmas to sum

rt-proofs!128 · created Feb 25, 2021 by Sergey Bozhko
- Merged
- 10
updated Mar 01, 2021
Additivity theory

rt-proofs!127 · created Feb 23, 2021 by Ghost User
- Merged
- 38
updated Mar 08, 2021
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
Added `bigcat` over sequences

rt-proofs!125 · created Feb 19, 2021 by Ghost User
- Merged
- 34
updated Mar 01, 2021
Ssrlia refactoring

rt-proofs!124 · created Jan 29, 2021 by Ghost User
- Merged
updated Jan 29, 2021
Sum refactoring

rt-proofs!123 · created Dec 14, 2020 by Ghost User
- Merged
- 3
- 1
updated Jan 02, 2021
Minor documentation changes about tactics.

rt-proofs!122 · created Nov 17, 2020 by Martin Constantino–Bodin
- Merged
- 1
updated Dec 11, 2020
Define completion sequences

rt-proofs!121 · created Sep 28, 2020 by Pierre Roux
Definition Discussion
- Merged
- 12
- Approved
updated Mar 08, 2021
optimize names for run-to-completion threshold functions

rt-proofs!120 · created Sep 25, 2020 by Sergey Bozhko
- Merged
- 2
updated Dec 11, 2020
generalize definition of busy interval

rt-proofs!119 · created Sep 25, 2020 by Sergey Bozhko
- Merged
- 1
updated Sep 25, 2020
Add [arrives_in] to [sequential_tasks] definition

rt-proofs!118 · created Sep 23, 2020 by Sergey Bozhko
- Merged
- 2
updated Sep 24, 2020
proof-state recorder tweaks and fixes

rt-proofs!117 · created Sep 22, 2020 by Björn Brandenburg
- Merged
updated Sep 22, 2020
Generalize ideal aRTA

rt-proofs!116 · created Sep 14, 2020 by Sergey Bozhko
- Merged
- 173
- Approved
updated Jan 23, 2023
Add setoid rewrite

rt-proofs!115 · created Sep 14, 2020 by Sergey Bozhko
- Merged
- 11
updated Jul 22, 2021