aboutsummaryrefslogtreecommitdiffstats
path: root/scheduling/BTL_Schedulerproof.v
Commit message (Collapse)AuthorAgeFilesLines
* remove todos, cleanLéo Gourdin2021-07-281-47/+0
|
* non trapping loadsLéo Gourdin2021-07-231-1/+1
|
* nothing admitted !!Léo Gourdin2021-07-221-1/+2
|
* expansions btl proofsLéo Gourdin2021-07-211-4/+2
|
* new expansion oracle for BTLLéo Gourdin2021-07-201-2/+4
|
* proof for symbolic simu, need to finish equiv_inputsLéo Gourdin2021-07-201-5/+3
|
* Finish implem proof, need to adapt scheduler proofLéo Gourdin2021-07-191-1/+2
|
* transf fct correct in BTL scheduler proofLéo Gourdin2021-06-201-5/+5
|
* finish main proofLéo Gourdin2021-06-191-18/+128
|
* lemma on eqregs?Léo Gourdin2021-06-181-13/+6
|
* End of main scheduling proofLéo Gourdin2021-06-181-54/+85
|
* some advance, new section to simplify context from symbolic execLéo Gourdin2021-06-171-60/+143
|
* some advance in sched proofLéo Gourdin2021-06-151-24/+92
|
* Preparation for scheduling proof, main lemmas okLéo Gourdin2021-06-141-13/+40
|
* begin scheduler BTL proofLéo Gourdin2021-06-141-5/+141
|
* stub match_statesSylvain Boulmé2021-06-111-1/+3
|
* remove dupmap from BTL_Scheduler !Sylvain Boulmé2021-05-281-0/+2
|
* archi pour la verif du schedulerSylvain Boulmé2021-05-281-0/+29
|
* starting to extend RTLtoBTL with Liveness checking (on BTL side)Sylvain Boulmé2021-05-281-0/+0