aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* 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* ↵Sylvain Boulmé2021-06-092-87/+42
| | | | simplifications (à venir )
* generalize nestedSylvain Boulmé2021-06-091-71/+74
|
* Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert ↵Sylvain Boulmé2021-06-081-28/+172
|\ | | | | | | into BTL
| * 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 ↵Léo Gourdin2021-06-073-27/+351
| |\ | | | | | | | | | into BTL
| * | 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 ↵Léo Gourdin2021-06-042-12/+115
|\ | | | | | | into BTL
| * 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 ↵Léo Gourdin2021-06-043-35/+77
|\ | | | | | | into BTL
| * 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 ↵Léo Gourdin2021-06-032-109/+112
|\ | | | | | | into BTL
| * Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert ↵Sylvain Boulmé2021-06-031-21/+112
| |\ | | | | | | | | | into BTL
| * | progress in BTL_SEsimurefSylvain Boulmé2021-06-032-109/+112
| | |
* | | update a more general version of the liveness checkerLéo Gourdin2021-06-031-93/+118
| |/ |/|
* | Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert ↵Léo Gourdin2021-06-022-176/+255
|\| | | | | | | into BTL
| * minor renamingSylvain Boulmé2021-06-021-9/+9
| |
| * fix the definition of [symbolic_simu] in BTL_SEtheorySylvain Boulmé2021-06-022-172/+251
| |
* | lemmas on entrypoint, tr_inputs, eqlive_regs, ...Léo Gourdin2021-06-021-21/+112
|/
* Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert ↵Léo Gourdin2021-06-024-111/+417
|\ | | | | | | into BTL
| * the current "high-level" specification of the simulation test will not work !Sylvain Boulmé2021-06-023-37/+124
| |
| * starting BTL_SEsimurefSylvain Boulmé2021-06-013-100/+319
| |
* | some advance in main liveness lemmasLéo Gourdin2021-06-021-28/+68
|/
* Some others main lemmasLéo Gourdin2021-06-011-7/+33
|
* preparing liveness proof main theoremLéo Gourdin2021-06-011-2/+43
|
* Lemma liveness_checker_correctLéo Gourdin2021-06-011-0/+12
|
* Lemma list_iblock_checker_correctLéo Gourdin2021-06-011-0/+20
|
* Dupmap bugfix and some advance in LivegenLéo Gourdin2021-05-316-30/+92
|
* Merge branch 'BTL' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy/CompCert ↵Léo Gourdin2021-05-311-19/+13
|\ | | | | | | into BTL
| * prove fsem2cfgsem_ibistep_simuSylvain Boulmé2021-05-311-19/+13
| |
* | remove accidentally pushed test scriptsLéo Gourdin2021-05-313-44/+0
|/
* BTL Scheduler oracle and some draftsLéo Gourdin2021-05-319-13/+136
|
* BTLroadmap: jumptableSylvain Boulmé2021-05-291-1/+1
|
* maj roadmapSylvain Boulmé2021-05-281-36/+32
|
* declare a checker for the symbolic simulationSylvain Boulmé2021-05-281-2/+13
|
* remove dupmap from BTL_Scheduler !Sylvain Boulmé2021-05-283-36/+22
|
* archi pour la verif du schedulerSylvain Boulmé2021-05-283-11/+82
|
* starting to extend RTLtoBTL with Liveness checking (on BTL side)Sylvain Boulmé2021-05-288-37/+99
|
* splitting BTL by introducing BTLmatchRTLSylvain Boulmé2021-05-287-635/+615
| | | | | reduce also copy-paste between BTLtoRTLproof and RTLtoBTLproof sharing is done in BTLmatchRTL
generated by cgit (git 2.34.1) at 2024-07-11 21:21:46 +0000