aboutsummaryrefslogtreecommitdiffstats
path: root/kvx
Commit message (Expand)AuthorAgeFilesLines
...
| * | | | | | | | | | | | | | Changing siexit_simu to be able to prove hsiexit_simu_core_correctCyril SIX2020-08-182-12/+9
| * | | | | | | | | | | | | | One part of hsiexit_simu_core_correctCyril SIX2020-08-181-37/+12
| * | | | | | | | | | | | | | Proof of hsilocal_simu_core_correctCyril SIX2020-08-181-5/+10
| * | | | | | | | | | | | | | None caseCyril SIX2020-08-181-3/+11
| * | | | | | | | | | | | | | Using PTree.combine to express picking register values from either rs0 or hstCyril SIX2020-08-181-10/+19
| * | | | | | | | | | | | | | Trying to modify definitions to include list of alive registersCyril SIX2020-08-171-45/+113
| | |_|_|/ / / / / / / / / / | |/| | | | | | | | | | | |
| * | | | | | | | | | | | | generalize builtin_arg_inj into builtin_arg_mapSylvain Boulmé2020-07-232-9/+10
| | |_|/ / / / / / / / / / | |/| | | | | | | | | | |
| * | | | | | | | | | | | Verificators of inclusionCyril SIX2020-07-221-206/+286
| * | | | | | | | | | | | Solving the hok problemCyril SIX2020-07-221-31/+14
| * | | | | | | | | | | | Branching simu_corebCyril SIX2020-07-221-211/+58
| * | | | | | | | | | | | hfinal_simu_coreCyril SIX2020-07-221-1/+70
| | |/ / / / / / / / / / | |/| | | | | | | | | |
| * | | | | | | | | | | ProgressCyril SIX2020-07-212-72/+109
| * | | | | | | | | | | hsistate_simu_core_correctCyril SIX2020-07-212-170/+183
| * | | | | | | | | | | ProgressCyril SIX2020-07-162-55/+207
| * | | | | | | | | | | fix hsilocal_simu_core_correctSylvain Boulmé2020-07-111-0/+38
| * | | | | | | | | | | Lemmas on hsilocal_simu ---> relies on reflexivity of istate_simu (which isn'...Cyril SIX2020-07-101-7/+64
| * | | | | | | | | | | fix commentSylvain Boulmé2020-07-101-1/+1
| * | | | | | | | | | | remove junk commentSylvain Boulmé2020-07-101-10/+0
| * | | | | | | | | | | try to fix refinement definition on exitsSylvain Boulmé2020-07-102-33/+78
| |/ / / / / / / / / /
| * | | | | | | | | | Merge branch 'mppa-RTLpathSE-verif-test-sfval_simu' into mppa-RTLpathSE-verifSylvain Boulmé2020-07-094-796/+1058
| |\ \ \ \ \ \ \ \ \ \ | | |/ / / / / / / / / | |/| | | | | | | | |
| | * | | | | | | | | adapting Cyril's proofs in RTLpathSE_impl for the new definitions of simu.Sylvain Boulmé2020-07-083-657/+525
| | * | | | | | | | | weaker sfval_simuSylvain Boulmé2020-07-083-134/+183
| | * | | | | | | | | Characterizing Op dependency on memorySylvain Boulmé2020-07-081-0/+39
| | * | | | | | | | | AvancementCyril SIX2020-07-072-88/+290
| | * | | | | | | | | ssem_final with less dependenciesCyril SIX2020-07-061-11/+14
| | * | | | | | | | | init_hsistate_correctCyril SIX2020-07-061-5/+29
| | * | | | | | | | | Version without dependency on rs0, m0, ge and sp ?Cyril SIX2020-07-031-44/+60
| * | | | | | | | | | hsexec_correct proved (under admitted lemmas).Sylvain Boulmé2020-07-031-68/+48
| |/ / / / / / / / /
| * | | | | | | | | Scope issue..Cyril SIX2020-07-031-11/+12
| * | | | | | | | | Fixing ge, sp, rs, m issueCyril SIX2020-07-031-8/+9
| * | | | | | | | | fix the proof sketchSylvain Boulmé2020-07-031-30/+22
| * | | | | | | | | sketch the proof of symbolic execution of one instructionSylvain Boulmé2020-07-032-35/+68
| * | | | | | | | | slightly simpler codeSylvain Boulmé2020-07-021-64/+88
| * | | | | | | | | Optimization of Iop symbolic executionSylvain Boulmé2020-07-022-35/+107
| * | | | | | | | | Fix hypothesis on environment in hsstate_simuSylvain Boulmé2020-07-021-3/+4
| * | | | | | | | | remove useless (and unprovable) lemmas on completeness of the refinementSylvain Boulmé2020-07-021-47/+66
| * | | | | | | | | Avancement, mais est-ce prouvable ?Cyril SIX2020-07-011-0/+37
| * | | | | | | | | hsexec_completeCyril SIX2020-07-011-37/+36
| * | | | | | | | | AvancementCyril SIX2020-07-012-74/+120
| * | | | | | | | | hsexec_correctCyril SIX2020-07-012-27/+138
| * | | | | | | | | Some renamingCyril SIX2020-07-011-38/+49
| * | | | | | | | | a minor commentSylvain Boulmé2020-06-301-2/+2
| * | | | | | | | | starting refinement of (abstract) symbolic executionsSylvain Boulmé2020-06-301-0/+160
| * | | | | | | | | Must generalize silocal_simub with a list of regsCyril SIX2020-06-291-3/+5
| * | | | | | | | | Only silocal_simub leftCyril SIX2020-06-291-132/+171
| * | | | | | | | | sfval_simub_correctCyril SIX2020-06-291-6/+175
| * | | | | | | | | Going further in sfval_simubCyril SIX2020-06-291-6/+60
| * | | | | | | | | sval_simub + sval_simub_correctCyril SIX2020-06-291-9/+51
| * | | | | | | | | Start of sval_simubCyril SIX2020-06-251-3/+93
| * | | | | | | | | Proving small lemmasCyril SIX2020-06-251-6/+33
generated by cgit (git 2.34.1) at 2024-07-12 08:17:13 +0000