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

Change definition of completion

!25 · created Jun 05, 2019 by Sergey Bozhko
- Merged
- 1
updated Jun 12, 2019
Port to ssreflect 1.9

!24 · created Jun 05, 2019 by Björn Brandenburg
- Merged
updated Jun 05, 2019
Naming conventions

!22 · created May 24, 2019 by Sophie Quinton
- Merged
- 10
updated Jun 05, 2019
Delete redundant busy_interval file

!23 · created May 26, 2019 by Sergey Bozhko
- Merged
- 1
updated Jun 04, 2019
Delete useless assumption in util-lemma

!21 · created May 19, 2019 by Sergey Bozhko
- Merged
- 1
updated May 20, 2019
Port more service and completion facts

!20 · created May 13, 2019 by Björn Brandenburg
- Merged
- 11
updated May 16, 2019
EDF instantiation of abstract RTA

!14 · created Apr 15, 2019 by Sergey Bozhko
- Merged
- 1
updated May 13, 2019
Initial service and completion facts

!18 · created May 07, 2019 by Björn Brandenburg
- Merged
- 2
updated May 13, 2019
Shorten a needlessly-long proof

!19 · created May 12, 2019 by Sergey Bozhko
- Merged
- 1
updated May 13, 2019
Base for the behavior part of refactored PROSA.

!12 · created Apr 12, 2019 by Maxime Lesourd
- Merged
- 45
updated May 07, 2019
Add comments in unil.sorting

!16 · created May 03, 2019 by Sergey Bozhko
- Merged
- 1
updated May 06, 2019
fix the proof of find_uniq under mathcomp version 1.8

!15 · created Apr 29, 2019 by Björn Brandenburg
- Merged
- 2
- 1
updated Apr 30, 2019
Complete proof of Abstract RTA

!9 · created Sep 21, 2018 by Sergey Bozhko
- Merged
- 35
updated Apr 05, 2019
Enable Gitlab Syntax Highlighting

!10 · created Oct 12, 2018 by Björn Brandenburg
- Merged
- 1
updated Oct 19, 2018
Improve proof of completion_monotonic lemma

!8 · created Sep 19, 2018 by Sophie Quinton
- Merged
- 2
updated Sep 20, 2018
Formalization of Weak Sustainability

!6 · created Feb 13, 2018 by Felipe Cerqueira
- Merged
updated Jul 17, 2018
Tdma

!2 · created Nov 14, 2017 by Xiaojie Guo
- Merged
- 38
updated Jan 05, 2018
Suspension-aware Scheduling

!3 · created Nov 22, 2017 by Felipe Cerqueira
- Merged
- 3
updated Dec 07, 2017
Make Prosa compatible with Coq 8.7 and Mathcomp 1.6.4

!4 · created Dec 07, 2017 by Felipe Cerqueira
- Merged
updated Dec 07, 2017
Fix Makefile on OS X

!1 · created Jul 13, 2016 by Björn Brandenburg
- Merged
- 1
updated Jul 14, 2016