Add citation

2 files changed, 14 insertions, 1 deletions

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}.
 
diff --git a/references.bib b/references.bib
index 5dc3ae5..3e2ed3d 100644
--- a/references.bib
+++ b/references.bib
@@ -333,3 +333,16 @@ url = {https://github.com/project-oak/silveroak},
 	pages = {857-858},
 	doi = {10.1145/1837274.1837489}
 }
+
+@InProceedings{appel11_verif_softw_toolc,
+	author = "Appel, Andrew W.",
+	editor = "Barthe, Gilles",
+	title = "Verified Software Toolchain",
+	booktitle = "Programming Languages and Systems",
+	year = "2011",
+	publisher = "Springer Berlin Heidelberg",
+	address = "Berlin, Heidelberg",
+	pages = "1--17",
+	abstract = "The software toolchain includes static analyzers to check assertions about programs; optimizing compilers to translate programs to machine language; operating systems and libraries to supply context for programs. Our Verified Software Toolchain verifies with machine-checked proofs that the assertions claimed at the top of the toolchain really hold in the machine-language program, running in the operating-system context, on a weakly-consistent-shared-memory machine.",
+	isbn = "978-3-642-19718-5"
+}