aboutsummaryrefslogtreecommitdiffstats
Commit message (Expand)AuthorAgeFilesLines
...
| | * | symbolic_simu impl definitionsLéo Gourdin2021-07-071-47/+9
| | * | hrexec1Léo Gourdin2021-07-071-27/+81
| | * | progress in simulation testLéo Gourdin2021-07-071-57/+250
| | * | Some advance, need to finish canonbuilding proofsLéo Gourdin2021-07-061-13/+270
| | * | lemma on HC_set_regLéo Gourdin2021-07-052-52/+165
| | * | red_PTree lemmasLéo Gourdin2021-07-012-10/+77
| | * | cbranch expanseLéo Gourdin2021-06-301-0/+25
| | * | coercions and simplifyLéo Gourdin2021-06-302-3/+91
| | * | some advanceLéo Gourdin2021-06-301-14/+154
| | * | Starting symbolic execution implementationLéo Gourdin2021-06-301-0/+314
| | * | BTLroadmap: combinaison liveness et invariants ?Sylvain Boulmé2021-06-251-9/+47
| | * | update BTLroadmapSylvain Boulmé2021-06-241-5/+6
| | * | 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-182-14/+7
| | * | finish RTLtoBTL proofLéo Gourdin2021-06-181-2/+18
| | * | End of main scheduling proofLéo Gourdin2021-06-183-59/+90
| | * | some advance, new section to simplify context from symbolic execLéo Gourdin2021-06-173-66/+151
| | * | some advance in sched proofLéo Gourdin2021-06-151-24/+92
| | * | Preparation for scheduling proof, main lemmas okLéo Gourdin2021-06-144-16/+41
| | * | begin scheduler BTL proofLéo Gourdin2021-06-142-5/+142
| | * | stub match_statesSylvain Boulmé2021-06-111-1/+3
| | * | add hid in BTL_SEtheory: this avoids duplication of types (and should not be ...Sylvain Boulmé2021-06-112-150/+157
| | * | Roadmap: precision sur le cout de verification des superblocksSylvain Boulmé2021-06-111-2/+9
| | * | Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...Sylvain Boulmé2021-06-11347-6030/+10566
| | |\ \
| | | * | remove filter fileLéo Gourdin2021-06-101-39/+0
| | | * | Merge branch 'kvx-work' into BTLLéo Gourdin2021-06-10346-5991/+10566
| | | |\ \
| | * | | | proving the remaining lemma for sexec_rec_okpreservSylvain Boulmé2021-06-111-123/+162
| | |/ / /
| | * | | theorem rexec_simu_correctSylvain Boulmé2021-06-101-25/+111
| | * | | fix rst_simu_correctSylvain Boulmé2021-06-101-27/+21
| | * | | remove historySylvain Boulmé2021-06-102-196/+121
| | * | | fix sstate_simuSylvain Boulmé2021-06-092-32/+35
| | * | | valid_pointer_preserv dans BTL_SEtheory => opportunites de *grosses* simplifi...Sylvain Boulmé2021-06-092-87/+42
| | * | | generalize nestedSylvain Boulmé2021-06-091-71/+74
| | * | | Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...Sylvain Boulmé2021-06-081-28/+172
| | |\ \ \
| | | * | | End of liveness proofLéo Gourdin2021-06-071-54/+45
| | | * | | ugly complete version of liveness proof (I will clean in next commits)Léo Gourdin2021-06-071-34/+40
| | | * | | Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...Léo Gourdin2021-06-073-27/+351
| | | |\ \ \
| | | * | | | advance for tr_input proofLéo Gourdin2021-06-071-24/+171
| | * | | | | preuve de rexec_rec_correct via les notions history/histOKSylvain Boulmé2021-06-081-41/+251
| | | |/ / / | | |/| | |
| | * | | | avancement ref de l'exe symboliqueSylvain Boulmé2021-06-072-26/+306
| | * | | | mSylvain Boulmé2021-06-061-1/+3
| | * | | | IDEE pour la STRENGTH-REDUCTIONSylvain Boulmé2021-06-061-1/+43
| | |/ / /
| | * | | Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...Léo Gourdin2021-06-042-12/+115
| | |\ \ \
| | | * | | starting refinement of symbolic executionSylvain Boulmé2021-06-042-12/+115
| | * | | | preparation and starting final lemmaLéo Gourdin2021-06-041-21/+100
| | |/ / /
| | * | | Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...Léo Gourdin2021-06-043-35/+77
| | |\ \ \
| | | * | | progress in BTL_SEsimurefSylvain Boulmé2021-06-043-35/+77
| | * | | | Some advance in Liveness lemmasLéo Gourdin2021-06-041-71/+138
| | |/ / /
| | * | | Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert int...Léo Gourdin2021-06-032-109/+112
| | |\ \ \
generated by cgit (git 2.34.1) at 2024-06-02 12:57:03 +0000