aboutsummaryrefslogtreecommitdiffstats
path: root/docs/index.org
diff options
context:
space:
mode:
Diffstat (limited to 'docs/index.org')
-rw-r--r--docs/index.org4
1 files changed, 2 insertions, 2 deletions
diff --git a/docs/index.org b/docs/index.org
index 7a92650..455a23a 100644
--- a/docs/index.org
+++ b/docs/index.org
@@ -1,5 +1,5 @@
-#+SETUPFILE: publish.setup
-#+TITLE: Vericert
+#+setupfile: publish.setup
+#+title: Vericert
A formally verified high-level synthesis (HLS) tool written in Coq, building on top of [[https://github.com/AbsInt/CompCert][CompCert]]. This ensures the correctness of the C to Verilog translation according to our Verilog semantics and CompCert's C semantics, removing the need to check the resulting hardware for behavioural correctness.