index
:
compcert-kvx
CPP22_if_lifting
CPP22_main
master
patched_for_velus
riscV-cmov
ssa
vericert
vericert-kvx
Unnamed repository; edit this file 'description' to name the repository.
about
summary
refs
log
tree
commit
diff
stats
log msg
author
committer
range
path:
root
/
scheduling
/
BTL_Schedulerproof.v
Commit message (
Expand
)
Author
Age
Files
Lines
*
expansions btl proofs
Léo Gourdin
2021-07-21
1
-4
/
+2
*
new expansion oracle for BTL
Léo Gourdin
2021-07-20
1
-2
/
+4
*
proof for symbolic simu, need to finish equiv_inputs
Léo Gourdin
2021-07-20
1
-5
/
+3
*
Finish implem proof, need to adapt scheduler proof
Léo Gourdin
2021-07-19
1
-1
/
+2
*
transf fct correct in BTL scheduler proof
Léo Gourdin
2021-06-20
1
-5
/
+5
*
finish main proof
Léo Gourdin
2021-06-19
1
-18
/
+128
*
lemma on eqregs?
Léo Gourdin
2021-06-18
1
-13
/
+6
*
End of main scheduling proof
Léo Gourdin
2021-06-18
1
-54
/
+85
*
some advance, new section to simplify context from symbolic exec
Léo Gourdin
2021-06-17
1
-60
/
+143
*
some advance in sched proof
Léo Gourdin
2021-06-15
1
-24
/
+92
*
Preparation for scheduling proof, main lemmas ok
Léo Gourdin
2021-06-14
1
-13
/
+40
*
begin scheduler BTL proof
Léo Gourdin
2021-06-14
1
-5
/
+141
*
stub match_states
Sylvain Boulmé
2021-06-11
1
-1
/
+3
*
remove dupmap from BTL_Scheduler !
Sylvain Boulmé
2021-05-28
1
-0
/
+2
*
archi pour la verif du scheduler
Sylvain Boulmé
2021-05-28
1
-0
/
+29
*
starting to extend RTLtoBTL with Liveness checking (on BTL side)
Sylvain Boulmé
2021-05-28
1
-0
/
+0