aboutsummaryrefslogtreecommitdiffstats
path: root/kvx/lib
Commit message (Expand)AuthorAgeFilesLines
* Merge branch 'kvx-test-prepass' of gricad-gitlab.univ-grenoble-alpes.fr:sixcy...David Monniaux2020-11-278-3404/+0
|\
| * fixing the move of the verified prepass scheduler into scheduling/ directorySylvain Boulmé2020-10-171-872/+0
| * Merge remote-tracking branch 'origin/kvx-test-prepass' into mppa-RTLpathSE-verifCyril SIX2020-10-1615-7426/+98
| |\
| * | removing useless opt_simuSylvain Boulmé2020-10-133-36/+25
| * | refactoring of RTLpathSE_impl.v (split with _simu_specs)Sylvain Boulmé2020-10-135-3911/+2086
| * | remove the last tiny issue!Sylvain Boulmé2020-10-121-10/+3
| * | simpl hsstate_simu_core_correctSylvain Boulmé2020-10-121-3/+1
| * | fix one issue by generalizing RTLpathSE_theory.sstate_simuSylvain Boulmé2020-10-122-9/+18
| * | move issue from hsexec_correct to hsstate_simu_core_correctSylvain Boulmé2020-10-121-14/+19
| * | most of the proof is done ! two (small ?) issues remain...Sylvain Boulmé2020-10-121-30/+83
| * | oops: forget to save before compile/commit/pushSylvain Boulmé2020-10-121-2/+5
| * | end of merge with Cyril's proofSylvain Boulmé2020-10-122-59/+227
| * | starting to merge with Cyril's proofSylvain Boulmé2020-10-111-48/+773
| * | hconsing: full proof of hsiexec_path_correctSylvain Boulmé2020-10-102-42/+71
| * | progress on hslocal_set_sreg_correctSylvain Boulmé2020-10-101-37/+53
| * | progress on hsexec_inst_correct_dynSylvain Boulmé2020-10-101-39/+140
| * | hconsing: red_PTree_set_correctSylvain Boulmé2020-10-091-0/+11
| * | hconsing: root_happly_correct + simplify_correct DONESylvain Boulmé2020-10-094-15/+145
| * | prove the kvx-test-prepass fix (commit 0e4186b8f)Sylvain Boulmé2020-10-081-14/+58
| * | Merge branch 'mppa-RTLpathSE-verif_Op_mem-irrel' into mppa-RTLpathSE-xverifSylvain Boulmé2020-10-081-30/+29
| |\ \
| | * | prove the trick of simplify (as implemented in RTLpathSE_impl_junk)Sylvain Boulmé2020-08-271-18/+6
| | * | prove that Mem.valid is preserved by symbolic execution of RTLpathSylvain Boulmé2020-08-271-12/+22
| * | | Restart the proof with cherry-pick from Cyril and commit 0e4186b8fSylvain Boulmé2020-10-082-1795/+433
| * | | Some theorem was wrongCyril SIX2020-09-301-4/+18
| * | | Proof of hsok_local_set_sregCyril SIX2020-09-301-4/+25
| * | | Some more progressCyril SIX2020-09-291-2/+33
| * | | Bit of progressCyril SIX2020-09-291-6/+40
| * | | Proof of simplify_correctCyril SIX2020-09-281-45/+101
| * | | A bit of new Ltac and renamingCyril SIX2020-09-211-23/+70
| * | | More avancementCyril SIX2020-09-181-3/+29
| * | | hsiexec_inst_correct_dyn proof of IopCyril SIX2020-09-181-1/+42
| * | | AvancementCyril SIX2020-09-181-29/+83
| * | | Some renamingCyril SIX2020-09-181-129/+230
| * | | Proof of sfval_simu_check_correctCyril SIX2020-09-151-14/+132
| * | | CleanupCyril SIX2020-09-091-4/+1
| * | | exec_final_correct provedCyril SIX2020-09-091-22/+122
| * | | Proving the last admit of ssem_final_simuCyril SIX2020-09-081-2/+24
| * | | hsexec_final_correct progressCyril SIX2020-09-071-2/+30
| * | | Proof of hfinal_simu_core_correctCyril SIX2020-09-074-35/+21
| * | | Proof of barg_proj_refines_eqCyril SIX2020-09-071-5/+43
| * | | Updates from _impl.v to _impl_junk.vCyril SIX2020-09-031-55/+102
| * | | Proof of hsilocal_simu_core_correct junkCyril SIX2020-09-031-14/+16
| * | | More proofsCyril SIX2020-09-031-8/+32
| * | | Proof of may_trap_correctCyril SIX2020-09-011-2/+15
| * | | Simplificating hsiexit_refines_statCyril SIX2020-09-011-7/+4
| * | | Proof of hsistate_simu_core_correctCyril SIX2020-09-011-6/+30
| * | | SUCCESS: prouve 1 des admit de hsistate_simu_core_correct.Sylvain Boulmé2020-08-281-14/+13
| * | | add nested_sok in hsistate_refines_dynSylvain Boulmé2020-08-281-35/+63
| * | | more realistic ok_allexit.Sylvain Boulmé2020-08-271-5/+5
| * | | reduction de la preuve de raffinement du exit à ok_allexitSylvain Boulmé2020-08-272-54/+81
| |/ /
generated by cgit (git 2.34.1) at 2024-07-04 14:09:24 +0000