~ymherklotz/vericert

A formally verified high-level synthesis tool based on CompCert and written in Coq.

3cca0fa Finish proofs in GiblePargenproofBackward.v

16 hours ago

cfeb4eb Add proofs of gather_predicates

a day ago
None