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

	Commit message (Collapse)	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