diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-06-03 12:21:17 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-06-03 12:21:17 +0100 |
commit | 8683616af94aa8cae82cdd07798941ca1f3180b0 (patch) | |
tree | 8396afa8860efe3fb437ac65b873a9a90f3fe2fe | |
parent | 16774a0bb03af846ce45f865f617c3c368b6c510 (diff) | |
download | oopsla21_fvhls-8683616af94aa8cae82cdd07798941ca1f3180b0.tar.gz oopsla21_fvhls-8683616af94aa8cae82cdd07798941ca1f3180b0.zip |
Add references
-rw-r--r-- | main.tex | 4 | ||||
-rw-r--r-- | references.bib | 16 |
2 files changed, 18 insertions, 2 deletions
@@ -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 diff --git a/references.bib b/references.bib new file mode 100644 index 0000000..dc73c13 --- /dev/null +++ b/references.bib @@ -0,0 +1,16 @@ +@article{leroy09_formal_verif_realis_compil, + author = {Leroy, Xavier}, + title = {Formal Verification of a Realistic Compiler}, + journal = {Commun. ACM}, + volume = 52, + number = 7, + pages = {107-115}, + year = 2009, + doi = {10.1145/1538788.1538814}, + address = {New York, NY, USA}, + issn = {0001-0782}, + issue_date = {July 2009}, + month = jul, + numpages = 9, + publisher = {ACM}, +} |