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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Fix imports in Coq modules	Yann Herklotz	2021-01-21	1	-8/+9
\|
*	Add correct copyright notices in files	Yann Herklotz	2021-01-10	1	-0/+19
\|
*	Fix build for Coq 8.12.1	Yann Herklotz	2020-11-26	1	-5/+4
\|
*	Update definition of Vneg	Yann Herklotz	2020-11-07	1	-1/+1
\|
*	Finish implementation of shrx_shrx_alt_equiv	Yann Herklotz	2020-11-05	1	-74/+133
\|
*	Proven with some assumptions	Yann Herklotz	2020-11-04	1	-4/+20
\|
*	Continue to prove signed_neg	Yann Herklotz	2020-11-04	1	-1/+44
\|
*	Add to Oshrximm proof	Yann Herklotz	2020-11-03	1	-55/+109
\|
*	Add intextra	Yann Herklotz	2020-11-03	1	-0/+115
\|
*	Change name to Vericert	Yann Herklotz	2020-07-14	1	-1/+1
\|
*	Define ofbytes	Yann Herklotz	2020-07-04	1	-1/+72
\|
*	Switch to uvalueToZ in lessdef.	James Pollard	2020-07-02	1	-23/+34
\|
*	Improve (?) automation.	James Pollard	2020-07-01	1	-8/+25
\|
*	Eliminate memory bounds assumption!	James Pollard	2020-06-29	1	-2/+2
\|
*	Finish first IStore proof (modulo some admissions).	James Pollard	2020-06-28	1	-12/+12
\|
*	Fix unsigned/signed issues.	James Pollard	2020-06-28	1	-13/+15
\|
*	Work on proof.	James Pollard	2020-06-28	1	-0/+50
\|
*	Finish ILoad proof with some assumptions:	James Pollard	2020-06-24	1	-184/+163
\| \| \| \| \| \|	* EXPR_OK: Yann to work on this. * READ_BOUNDS: To axiomise (or find a better solution). * 32-bit range of register values.
*	Normalise entire expression to avoid overflow issues.	James Pollard	2020-06-23	1	-0/+235