aboutsummaryrefslogtreecommitdiffstats
path: root/scheduling/BTL_SEsimuref.v
Commit message (Expand)AuthorAgeFilesLines
* Merge remote-tracking branch 'absint/master' into towards_3.10David Monniaux2021-12-011-6/+3
* non trapping loadsLéo Gourdin2021-07-231-6/+3
* branches expansions supportLéo Gourdin2021-07-221-5/+5
* lemma on HC_set_regLéo Gourdin2021-07-051-0/+11
* red_PTree lemmasLéo Gourdin2021-07-011-0/+6
* coercions and simplifyLéo Gourdin2021-06-301-1/+1
* add hid in BTL_SEtheory: this avoids duplication of types (and should not be ...Sylvain Boulmé2021-06-111-23/+15
* 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-101-188/+111
* fix sstate_simuSylvain Boulmé2021-06-091-31/+18
* valid_pointer_preserv dans BTL_SEtheory => opportunites de *grosses* simplifi...Sylvain Boulmé2021-06-091-66/+13
* generalize nestedSylvain Boulmé2021-06-091-71/+74
* 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-071-19/+302
* starting refinement of symbolic executionSylvain Boulmé2021-06-041-3/+106
* progress in BTL_SEsimurefSylvain Boulmé2021-06-041-12/+44
* progress in BTL_SEsimurefSylvain Boulmé2021-06-031-78/+58
* fix the definition of [symbolic_simu] in BTL_SEtheorySylvain Boulmé2021-06-021-108/+8
* the current "high-level" specification of the simulation test will not work !Sylvain Boulmé2021-06-021-26/+68
* starting BTL_SEsimurefSylvain Boulmé2021-06-011-0/+317
generated by cgit (git 2.34.1) at 2024-05-09 02:03:50 +0000