vericert - Vericert is a formally verified high-level synthesis tool.

	Commit message (Collapse)	Author	Age	Files	Lines
*	Annonimize submissiondev/asplos	Yann Herklotz	2023-08-10	1	-1/+1
\|
*	Work on scheduling proof	Yann Herklotz	2023-05-16	1	-0/+4
\|
*	Split proof up into more files	Yann Herklotz	2023-05-09	1	-1760/+64
\|
*	Add assumption and prove assumption that preds are evaluable	Yann Herklotz	2023-05-06	1	-43/+49
\|
*	Add check for mutexcl and fix top-level proof	Yann Herklotz	2023-05-06	1	-324/+47
\|
*	Finished proof of beq_pred_expr in both directions	Yann Herklotz	2023-05-05	1	-12/+108
\|
*	Finish forward and backward proofs for predicated proof	Yann Herklotz	2023-05-05	1	-189/+499
\|
*	Try and prove equivalence of predicated things	Yann Herklotz	2023-05-05	1	-167/+188
\|
*	Continue proofs about Abstr.v	Yann Herklotz	2023-05-04	1	-247/+311
\|
*	Fix definitions of structural equality	Yann Herklotz	2023-05-02	1	-18/+125
\|
*	Change nat to positive in Sat proof	Yann Herklotz	2023-04-27	1	-15/+12
\|
*	Added lemmas about decidability of Sat	Yann Herklotz	2023-04-24	1	-54/+189
\|
*	Add temp files	Yann Herklotz	2023-03-12	1	-4/+6
\|
*	Work on proof of norm_expression	Yann Herklotz	2023-02-22	1	-0/+178
\|
*	Change evaluation of predicates and remove forest_evaluable	Yann Herklotz	2023-02-11	1	-12/+16
\|
*	Switch to half lazy evaluation	Yann Herklotz	2023-02-05	1	-8/+28
\|
*	Prove top level theorems with evaluability	Yann Herklotz	2022-11-15	1	-0/+11
\|
*	Clean up proofs	Yann Herklotz	2022-10-11	1	-0/+10
\|
*	[sched] Remove some unprovable lemmas	Yann Herklotz	2022-10-06	1	-19/+42
\|
*	Update and fix the transformation	Yann Herklotz	2022-08-05	1	-3/+3
\|
*	Add back changes to Abstr	Yann Herklotz	2022-08-04	1	-185/+297
\|
*	Add forest type	Yann Herklotz	2022-08-01	1	-3/+8
\|
*	Merge remote-tracking branch 'origin/dev/scheduling' into dev/scheduling	Yann Herklotz	2022-07-31	1	-111/+4
\|\
\| *	Add current changes	Yann Herklotz	2022-07-31	1	-111/+4
\| \|
* \|	Start refactor in Abstr	Yann Herklotz	2022-07-31	1	-14/+29
\|/
*	Work on implementing abstract predicates	Yann Herklotz	2022-07-19	1	-99/+103
\|
*	Add work on abstract predicates	Yann Herklotz	2022-07-14	1	-44/+141
\|
*	Add work on scheduling	Yann Herklotz	2022-07-03	1	-18/+29
\|
*	Work on CondElim proof	Yann Herklotz	2022-06-03	1	-5/+5
\|
*	Rewrite a lot fixing scheduling of Gible	Yann Herklotz	2022-05-27	1	-120/+6
\|
*	Remove literal files again	Yann Herklotz	2022-03-26	1	-18/+36
\|
*	Move forall_ptree into common	Yann Herklotz	2022-03-22	1	-42/+0
\|
*	Add back proof of beq2_correct	Yann Herklotz	2022-03-03	1	-23/+76
\|
*	Fix Abstr	Yann Herklotz	2022-03-03	1	-30/+17
\|
*	Fix up some more documentation	Yann Herklotz	2022-02-25	1	-26/+13
\|
*	Add the tseytin transformation instead	Yann Herklotz	2021-11-14	1	-9/+0
\|
*	Add Admitted theorems for existence proofs	Yann Herklotz	2021-11-01	1	-9/+2
\|
*	Add construction of state in sem	Yann Herklotz	2021-10-31	1	-23/+147
\|
*	Make Abstr pass with admitted to check top-level	Yann Herklotz	2021-10-30	1	-45/+110
\|
*	Remove admitted from subproof	Yann Herklotz	2021-10-29	1	-6/+57
\|
*	Add intermediate step in proof of sem pres	Yann Herklotz	2021-10-27	1	-24/+82
\|
*	Work more on equivalence of SAT	Yann Herklotz	2021-10-26	1	-33/+121
\|
*	Continue on semantics preservation proof	Yann Herklotz	2021-10-24	1	-198/+178
\|
*	Add setoid typeclass	Yann Herklotz	2021-10-21	1	-15/+21
\|
*	Add work towards decidability of SAT solver	Yann Herklotz	2021-10-21	1	-29/+98
\|
*	Start to prove termination of SAT	Yann Herklotz	2021-10-20	1	-8/+0
\|
*	Continuations on proof of predicates	Yann Herklotz	2021-10-19	1	-98/+151
\|
*	[sched] Add combination of equivalent expressions	Yann Herklotz	2021-10-14	1	-10/+40
\|
*	[sched] Finish det proofs of basic Abstr semantics	Yann Herklotz	2021-10-13	1	-27/+44
\|
*	[sched] Add more proof to sem_pred_det	Yann Herklotz	2021-10-13	1	-1/+6
\|