Add to proof section

1 files changed, 41 insertions, 0 deletions

diff --git a/references.bib b/references.bib
index ec8e945..7df5cbe 100644
--- a/references.bib
+++ b/references.bib
@@ -639,3 +639,44 @@ year = {2020},
   year            = 1999,
   pages           = {7--es},
 }
+
+@inproceedings{loow19_verif_compil_verif_proces,
+	author = {L\"{o}\"{o}w, Andreas and Kumar, Ramana and Tan, Yong Kiam and
+                  Myreen, Magnus O. and Norrish, Michael and Abrahamsson, Oskar
+                  and Fox, Anthony},
+	title = {Verified Compilation on a Verified Processor},
+	tags = {verification},
+	booktitle = {Proceedings of the 40th ACM SIGPLAN Conference on Programming
+                  Language Design and Implementation},
+	year = 2019,
+	pages = {1041--1053},
+	doi = {10.1145/3314221.3314622},
+	url = {https://doi.org/10.1145/3314221.3314622},
+	acmid = 3314622,
+	address = {New York, NY, USA},
+	isbn = {978-1-4503-6712-7},
+	keywords = {compiler verification, hardware verification, program
+                  verification, verified stack},
+	location = {Phoenix, AZ, USA},
+	numpages = 13,
+	publisher = {ACM},
+	series = {PLDI 2019}
+}
+
+@inproceedings{loow19_proof_trans_veril_devel_hol,
+	author = {L\"{o}\"{o}w, Andreas and Myreen, Magnus O.},
+	title = {A Proof-producing Translator for Verilog Development in HOL},
+	tags = {hls, semantics},
+	booktitle = {Proceedings of the 7th International Workshop on Formal
+                  Methods in Software Engineering},
+	year = 2019,
+	pages = {99--108},
+	doi = {10.1109/FormaliSE.2019.00020},
+	url = {https://doi.org/10.1109/FormaliSE.2019.00020},
+	acmid = 3338828,
+	address = {Piscataway, NJ, USA},
+	location = {Montreal, Quebec, Canada},
+	numpages = 10,
+	publisher = {IEEE Press},
+	series = {FormaliSE '19}
+}