From 4aaeb6659756407b1373177fdb07f72ff6e82447 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Tue, 9 Jun 2020 11:24:45 +0100
Subject: Add response

---
 main.tex | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'main.tex')

diff --git a/main.tex b/main.tex
index 26916b6..4ef0593 100644
--- a/main.tex
+++ b/main.tex
@@ -199,11 +199,14 @@ Using CompCert, we can therefore build a fully verified high-level synthesis too
 
 \JW{Some papers to cite somewhere:
 \begin{itemize}
-    \item \citet{kundu+08} have done translation validation on an HLS tool called SPARK.
-    \item \citet{chapman+92} have proved (manually, as far as JW can tell) that the front-end and scheduler of the BEDROC synthesis system is correct. (NB: Chapman also wrote a PhD thesis about this (1994) but it doesn't appear to be online.)
+    \item \citet{kundu08_valid_high_level_synth} have done translation validation on an HLS tool called SPARK.\@
+    \item \citet{chapman92_verif_bedroc} have proved (manually, as far as JW can tell) that the front-end and scheduler of the BEDROC synthesis system is correct. (NB:\@ Chapman also wrote a PhD thesis about this (1994) but it doesn't appear to be online.)
 \end{itemize}
 }
 
+
+\YH{Amazing, thank you, yes it seems like Kundu \textit{et al.} have quite a few papers on formal verification of HLS algorithms using translation validation, as well as~\citet{karfa06_formal_verif_method_sched_high_synth}, all using the SPARK~\cite{gupta03_spark} synthesis tool.  And yes thank you, will definitely cite that paper.  There seem to be similar early proofs of high-level synthesis like~\citet{hwang91_formal_approac_to_sched_probl}.}
+
 \section{Verilog Semantics}
 
 Definition of state.
-- 
cgit 

