compcert-kvx - Unnamed repository; edit this file 'description' to name the repository.

	Commit message (Expand)	Author	Age	Files	Lines
*	remove todos, clean	Léo Gourdin	2021-07-28	1	-0/+46
*	nothing admitted !!	Léo Gourdin	2021-07-22	1	-16/+23
*	expansions btl proofs	Léo Gourdin	2021-07-21	1	-1/+1
*	new expansion oracle for BTL	Léo Gourdin	2021-07-20	1	-1/+1
*	Fix compile on ARM/x86 backends	Léo Gourdin	2021-07-20	1	-22/+20
*	proof for symbolic simu, need to finish equiv_inputs	Léo Gourdin	2021-07-20	1	-8/+9
*	Finish implem proof, need to adapt scheduler proof	Léo Gourdin	2021-07-19	1	-3/+54
*	lemma on eqregs?	Léo Gourdin	2021-06-18	1	-1/+1
*	End of main scheduling proof	Léo Gourdin	2021-06-18	1	-0/+1
*	some advance, new section to simplify context from symbolic exec	Léo Gourdin	2021-06-17	1	-5/+7
*	Preparation for scheduling proof, main lemmas ok	Léo Gourdin	2021-06-14	1	-1/+0
*	begin scheduler BTL proof	Léo Gourdin	2021-06-14	1	-0/+1
*	progress in BTL_SEsimuref	Sylvain Boulmé	2021-06-04	1	-0/+22
*	the current "high-level" specification of the simulation test will not work !	Sylvain Boulmé	2021-06-02	1	-1/+8
*	BTL Scheduler oracle and some drafts	Léo Gourdin	2021-05-31	1	-0/+2
*	declare a checker for the symbolic simulation	Sylvain Boulmé	2021-05-28	1	-2/+13
*	remove dupmap from BTL_Scheduler !	Sylvain Boulmé	2021-05-28	1	-22/+10
*	archi pour la verif du scheduler	Sylvain Boulmé	2021-05-28	1	-0/+40
*	starting to extend RTLtoBTL with Liveness checking (on BTL side)	Sylvain Boulmé	2021-05-28	1	-0/+0