Vericert 1.2.2

Mainly fix some documentation and remove any Admitted theorems, even though
these were in parts of the compiler that were never used.

Vericert 1.2.1

Main release for OOPSLA'21 paper.

• Add better documentation on how to run Vericert.
• Add Dockerfile with instructions on how to get figures of the paper.

Vericert 1.2.0

Features

• Added memory inferrence support and proof.

Vericert 1.1.0

Add a stable release with all proofs completed.

Vericert 1.0.1

Vericert 1.0.1

Release a new minor version fixing all proofs and fixing scripts to generate the badges.

Vericert 1.0.0

First release of a fully verified version of Vericert with support for the translation of many C constructs to Verilog.

Feature Support

• Most int instructions and operators.
• Non-recursive function calls.
• Local arrays, structs and unions of type int.
• Pointer arithmetic with int.

MVP: Working HLS without proofs

This is the first release with working HLS but without any proofs associated with it.