Merge requests · RT-PROOFS

eliminate ideal uniprocessor assumption from preemption-model facts

rt-proofs!284 · created Apr 03, 2023 by Björn Brandenburg
updated Apr 05, 2023
revise ELF<->FP generality claim

rt-proofs!286 · created Apr 04, 2023 by Björn Brandenburg
- Merged
- 1
- Approved
updated Apr 05, 2023
ELF Generality

rt-proofs!282 · created Mar 30, 2023 by Meenal Gupta
- Merged
- 16
- Approved
updated Apr 04, 2023
CI: check that POET certificates keep working

rt-proofs!283 · created Apr 01, 2023 by Björn Brandenburg
updated Apr 03, 2023
Adjust to prosa changes

POET!1 · created Apr 01, 2023 by Björn Brandenburg
updated Apr 01, 2023
more ideal uniprocessor cleanup

rt-proofs!280 · created Mar 30, 2023 by Björn Brandenburg
- Merged
- 5
updated Mar 30, 2023
add a workload partitioning lemma

rt-proofs!281 · created Mar 30, 2023 by Björn Brandenburg
- Merged
- 5
- 1
- Approved
updated Mar 30, 2023
introduce the class of sequential readiness models

rt-proofs!277 · created Mar 29, 2023 by Björn Brandenburg
- Merged
- Approved
updated Mar 30, 2023
fix CoqdocJS handling of apostrophes embedded in identifiers

rt-proofs!275 · created Mar 27, 2023 by Björn Brandenburg
- Merged
- 1
updated Mar 27, 2023
note some of GEL's generalizing properties

rt-proofs!274 · created Mar 23, 2023 by Björn Brandenburg
- Merged
- 18
updated Mar 24, 2023
fix `make vacuum` if no `_CoqProject` is present

rt-proofs!273 · created Mar 23, 2023 by Björn Brandenburg
- Merged
- 1
updated Mar 23, 2023
Bump MathComp lower bound to >= 1.16.0 and Coq to >= 8.16.

rt-proofs!272 · created Mar 17, 2023 by Pierre Roux
- Merged
- 5
updated Mar 17, 2023
Put mangle-names in a separate CI target

rt-proofs!271 · created Mar 16, 2023 by Pierre Roux
- Merged
- 1
updated Mar 16, 2023
Add a CI target testing mangle names

rt-proofs!266 · created Mar 01, 2023 by Pierre Roux
- Merged
- 1
updated Mar 16, 2023
Use mathcomp's int instead of stdlib's Z

rt-proofs!259 · created Feb 17, 2023 by Pierre Roux
- Merged
- 10
updated Mar 16, 2023
Move interference definitions out of ideal/iw_instantiation.v

rt-proofs!264 · created Feb 27, 2023 by Pierre Roux
- Merged
- 13
updated Mar 16, 2023
ELF Definition

rt-proofs!270 · created Mar 13, 2023 by Meenal Gupta
- Merged
- 76
updated Mar 15, 2023
priority relations and conversions for fp and jlfp

rt-proofs!268 · created Mar 03, 2023 by Meenal Gupta
- Merged
- 43
updated Mar 13, 2023
also spell-check *.md files

rt-proofs!267 · created Mar 02, 2023 by Björn Brandenburg
updated Mar 04, 2023
Add a warning about implicit arguments in guidelines

rt-proofs!260 · created Feb 17, 2023 by Pierre Roux
- Merged
- 9
updated Mar 02, 2023