Skip to content
GitLab
Explore
Sign in
RT-PROOFS
PROSA - Formally Proven Schedulability Analysis
Merge requests
Open
10
Merged
320
Closed
40
All
370
Actions
Subscribe to RSS feed
Recent searches
{{formattedKey}}
{{ title }}
{{ help }}
{{name}}
@{{username}}
None
Any
{{name}}
@{{username}}
None
Any
{{name}}
@{{username}}
None
Any
{{name}}
@{{username}}
None
Any
Upcoming
Started
{{title}}
None
Any
{{title}}
None
Any
{{title}}
None
Any
{{name}}
Yes
No
Yes
No
{{title}}
{{title}}
{{title}}
Title
Generalize one lemma
!327
· created
Oct 19, 2023
by
Kimaya Bedarkar
Merged
Approved
121
updated
Feb 14, 2024
Generalize one proof related to FP
!246
· created
Sep 05, 2022
by
Kimaya Bedarkar
Merged
1
updated
Sep 07, 2022
generalize preemption_time and priority-model compliance to any processor model
!276
· created
Mar 27, 2023
by
Björn Brandenburg
Merged
Approved
15
updated
Apr 14, 2023
Generalize priority inversion
!171
· created
Nov 11, 2021
by
Sergey Bozhko
Merged
51
updated
Sep 07, 2022
generalize proof and improve structure
!346
· created
Jan 15, 2024
by
Sergey Bozhko
Merged
5
updated
Jan 16, 2024
Guidelines
!100
· created
Jun 23, 2020
by
Ghost User
Merged
0
updated
Jun 30, 2020
Ideal Uniprocessor Scheduler Implementation
!96
· created
Apr 03, 2020
by
Björn Brandenburg
Merged
22
updated
Aug 26, 2020
Import ssreflect only once
!325
· created
Oct 11, 2023
by
Sergey Bozhko
Merged
1
updated
Oct 13, 2023
improve `busy_intervals_are_bounded_by` definition
!223
· created
Jun 30, 2022
by
Björn Brandenburg
Merged
0
updated
Jun 30, 2022
Improve documentation in restructuring/behavior
!65
· created
Nov 18, 2019
by
Björn Brandenburg
Merged
0
updated
Nov 18, 2019
Improve proof of completion_monotonic lemma
!8
· created
Sep 19, 2018
by
Sophie Quinton
Merged
2
0
updated
Sep 20, 2018
improve readability of `service_on` in ideal uniprocessor model
!199
· created
Mar 11, 2022
by
Björn Brandenburg
Merged
0
updated
Mar 11, 2022
Improve SBF-definition structure
!340
· created
Jan 05, 2024
by
Sergey Bozhko
Merged
9
updated
Jan 06, 2024
Improve tactic `convert_two_instants_into_instant_and_duration`
!153
· created
Oct 01, 2021
by
Sergey Bozhko
Merged
1
updated
Oct 05, 2021
improve terminology about priority inversion
!342
· created
Jan 10, 2024
by
Sergey Bozhko
Merged
1
updated
Jan 10, 2024
Initial service and completion facts
!18
· created
May 07, 2019
by
Björn Brandenburg
Merged
2
updated
May 13, 2019
Integrate rt_eauto into done (hence by and //)
!299
· created
Apr 19, 2023
by
Pierre Roux
Merged
3
updated
Apr 19, 2023
Introduce [rt_auto] and [rt_eauto] tactics
!198
· created
Mar 09, 2022
by
Sergey Bozhko
Merged
21
updated
Mar 18, 2022
Introduce eta-max vector
!161
· created
Oct 08, 2021
by
Sergey Bozhko
Merged
15
updated
Jan 13, 2022
Introduce notion of service inversion
!339
· created
Jan 04, 2024
by
Sergey Bozhko
Merged
75
updated
Jan 10, 2024
Prev
1
…
5
6
7
8
9
10
11
12
13
…
16
Next