From 42971f475053f87938f66b6cbb3d61c046b78ebe Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Thu, 25 Feb 2021 20:11:20 +0000
Subject: Add citation

---
 main.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'main.tex')

diff --git a/main.tex b/main.tex
index e29e927..1bd4fcc 100644
--- a/main.tex
+++ b/main.tex
@@ -209,7 +209,7 @@ There are many optimisations that need to be added to \vericert{} to turn it int
 
 \paragraph{Response:} It is true that a verified tool is still allowed to fail at compile time, meaning none of the correctness proofs need to hold if no output is produced.  However, this is mostly a matter of putting more engineering work into the tool to make it more complete.  Bugs are easier to identify as they will induce tool failures at compile time.
 
-In addition to that, specifically for an HLS tool taking C as input, undefined behaviour in the input code will allow the HLS tool to behave any way it wishes.  This becomes even more important when passing the C to a verified HLS tool, because if it is not free of undefined behaviour, then none of the proofs will hold.  Extra steps therefore need to be performed to ensure that the input is free of any undefined behaviour. 
+In addition to that, specifically for an HLS tool taking C as input, undefined behaviour in the input code will allow the HLS tool to behave any way it wishes.  This becomes even more important when passing the C to a verified HLS tool, because if it is not free of undefined behaviour, then none of the proofs will hold.  Extra steps therefore need to be performed to ensure that the input is free of any undefined behaviour, by using a tool like VST~\cite{appel11_verif_softw_toolc} for example.
 
 Finally, the input and output language semantics also need to be trusted, as the proofs only hold as long as the semantics are a faithful representation of the languages.  In \vericert{} this comes down to trusting the C semantics developed by \compcert{}~\cite{blazy09_mechan_seman_cligh_subset_c_languag} and the Verilog semantics, which we adapted from \citet{loow19_proof_trans_veril_devel_hol}.
 
-- 
cgit 

