Commit message (Expand) | Author | Age | Files | Lines | |
---|---|---|---|---|---|
* | lemma on eqregs? | Léo Gourdin | 2021-06-18 | 1 | -1/+1 |
* | End of main scheduling proof | Léo Gourdin | 2021-06-18 | 1 | -0/+1 |
* | some advance, new section to simplify context from symbolic exec | Léo Gourdin | 2021-06-17 | 1 | -5/+7 |
* | Preparation for scheduling proof, main lemmas ok | Léo Gourdin | 2021-06-14 | 1 | -1/+0 |
* | begin scheduler BTL proof | Léo Gourdin | 2021-06-14 | 1 | -0/+1 |
* | progress in BTL_SEsimuref | Sylvain Boulmé | 2021-06-04 | 1 | -0/+22 |
* | the current "high-level" specification of the simulation test will not work ! | Sylvain Boulmé | 2021-06-02 | 1 | -1/+8 |
* | BTL Scheduler oracle and some drafts | Léo Gourdin | 2021-05-31 | 1 | -0/+2 |
* | declare a checker for the symbolic simulation | Sylvain Boulmé | 2021-05-28 | 1 | -2/+13 |
* | remove dupmap from BTL_Scheduler ! | Sylvain Boulmé | 2021-05-28 | 1 | -22/+10 |
* | archi pour la verif du scheduler | Sylvain Boulmé | 2021-05-28 | 1 | -0/+40 |
* | starting to extend RTLtoBTL with Liveness checking (on BTL side) | Sylvain Boulmé | 2021-05-28 | 1 | -0/+0 |