diff options
| -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}, +} |