aboutsummaryrefslogtreecommitdiffstats
path: root/scheduling
Commit message (Expand)AuthorAgeFilesLines
* expansions btl proofsLéo Gourdin2021-07-214-8/+10
* new expansion oracle for BTLLéo Gourdin2021-07-203-4/+8
* Fix compile on ARM/x86 backendsLéo Gourdin2021-07-203-217/+28
* op simplify BTL introLéo Gourdin2021-07-201-9/+7
* proof for symbolic simu, need to finish equiv_inputsLéo Gourdin2021-07-203-23/+31
* Finish implem proof, need to adapt scheduler proofLéo Gourdin2021-07-193-113/+371
* hrexec_correct1Léo Gourdin2021-07-081-25/+48
* some progress in canonbuildingLéo Gourdin2021-07-071-14/+106
* 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-114-39/+43
|\
| * Merge branch 'kvx-work' into BTLLéo Gourdin2021-06-104-39/+43
| |\
| | * Merge remote-tracking branch 'origin/kvx-work' into merge_master_8.13.1Cyril SIX2021-06-017-31/+24
| | |\
| | * | replacing omega with lia in some fileLéo Gourdin2021-03-294-39/+43
* | | | 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
generated by cgit (git 2.34.1) at 2024-06-02 23:13:38 +0000