| Commit message (Expand) | Author | Age | Files | Lines | |
|---|---|---|---|---|---|
| * | remove todos, clean | Léo Gourdin | 2021-07-28 | 1 | -47/+0 |
| * | non trapping loads | Léo Gourdin | 2021-07-23 | 1 | -1/+1 |
| * | nothing admitted !! | Léo Gourdin | 2021-07-22 | 1 | -1/+2 |
| * | 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 |
 |
index : compcert-kvx | |
| Unnamed repository; edit this file 'description' to name the repository. |
| aboutsummaryrefslogtreecommitdiffstats |