Merge requests · RT-PROOFS

introduce the class of sequential readiness models

rt-proofs!277 · created Mar 29, 2023 by Björn Brandenburg
- Merged
- Approved
updated Mar 30, 2023
generalize preemption_time and priority-model compliance to any processor model

rt-proofs!276 · created Mar 27, 2023 by Björn Brandenburg
- Merged
- 15
- Approved
updated Apr 14, 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
ELF Definition

rt-proofs!270 · created Mar 13, 2023 by Meenal Gupta
- Merged
- 76
updated Mar 15, 2023
Draft: Definition of ELF

rt-proofs!269 · created Mar 13, 2023 by Meenal Gupta
- Closed
updated Mar 13, 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 CI target testing mangle names

rt-proofs!266 · created Mar 01, 2023 by Pierre Roux
- Merged
- 1
updated Mar 16, 2023
Draft: ELF-Definition

rt-proofs!265 · created Feb 28, 2023 by Meenal Gupta
- Closed
- 41
- Approved
updated Mar 13, 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
Rewrite create_makefile.sh as a Makefile

rt-proofs!263 · created Feb 27, 2023 by Pierre Roux
- Merged
- 2
updated Feb 28, 2023
Factorize two proofs

rt-proofs!262 · created Feb 24, 2023 by Pierre Roux
- Merged
- 2
- Approved
updated Feb 28, 2023
define restricted supply processor model

rt-proofs!261 · created Feb 24, 2023 by Sergey Bozhko
- Merged
- 42
updated Dec 12, 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
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
Fix implicit arguments in model/priority/classes.v

rt-proofs!258 · created Feb 16, 2023 by Pierre Roux
- Merged
- 11
- 1
- Approved
updated Feb 27, 2023