summaryrefslogtreecommitdiffstats
path: root/main.tex
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2020-06-03 12:21:17 +0100
committerYann Herklotz <git@yannherklotz.com>2020-06-03 12:21:17 +0100
commit8683616af94aa8cae82cdd07798941ca1f3180b0 (patch)
tree8396afa8860efe3fb437ac65b873a9a90f3fe2fe /main.tex
parent16774a0bb03af846ce45f865f617c3c368b6c510 (diff)
downloadoopsla21_fvhls-8683616af94aa8cae82cdd07798941ca1f3180b0.tar.gz
oopsla21_fvhls-8683616af94aa8cae82cdd07798941ca1f3180b0.zip
Add references
Diffstat (limited to 'main.tex')
-rw-r--r--main.tex4
1 files changed, 2 insertions, 2 deletions
diff --git a/main.tex b/main.tex
index 78c2403..858e916 100644
--- a/main.tex
+++ b/main.tex
@@ -149,7 +149,7 @@
%% Note: \begin{abstract}...\end{abstract} environment must come
%% before \maketitle command
\begin{abstract}
-Text of abstract \ldots.
+ We propose a formally verified HLS flow based on CompCert~\cite{leroy09_formal_verif_realis_compil}, by adding a Verilog backend which is a language used to describe hardware.
\end{abstract}
@@ -211,7 +211,7 @@ Text of paper \ldots
%% Bibliography
-%\bibliography{bibfile}
+\bibliography{references.bib}
%% Appendix