Add more to algorithm section

1 files changed, 52 insertions, 17 deletions

diff --git a/references.bib b/references.bib
index 29bd581..cb7f441 100644
--- a/references.bib
+++ b/references.bib
@@ -382,19 +382,6 @@
   title           = {Synthesis and Optimization of Digital Circuits},
   year            = 1994,
   publisher       = {McGraw-Hill Higher Education},
-  abstract        = {From the Publisher:Synthesis and Optimization of Digital Circuits offers a
-                  modern, up-to-date look at computer-aided design (CAD) of very large-scale
-                  integration (VLSI) circuits. In particular, this book covers techniques for
-                  synthesis and optimization of digital circuits at the architectural and logic
-                  levels, i.e., the generation of performance-and/or area-optimal circuits
-                  representations from models in hardware description languages. The book provides a
-                  thorough explanation of synthesis and optimization algorithms accompanied by a
-                  sound mathematical formulation and a unified notation. The text covers the
-                  following topics: modern hardware description languages (e.g., VHDL, Verilog);
-                  architectural-level synthesis of data flow and control units, including algorithms
-                  for scheduling and resource binding; combinational logic optimization algorithms
-                  for two-level and multiple-level circuits; sequential logic optimization methods;
-                  and library binding techniques, including those applicable to FPGAs.},
   edition         = {1st},
   isbn            = 0070163332,
 }
@@ -469,7 +456,7 @@
 
 @inproceedings{bourgeat20_essen_blues,
   author          = {Bourgeat, Thomas and Pit-Claudel, Cl\'{e}ment and Chlipala, Adam and Arvind},
-  title           = {The Essence of Bluespec: A Core Language for Rule-Based Hardware Design},
+  title           = {The Essence of {Bluespec}: A Core Language for Rule-Based Hardware Design},
   booktitle       = {Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design
                   and Implementation},
   year            = 2020,
@@ -487,7 +474,7 @@
 
 @inproceedings{yang11_findin_under_bugs_c_compil,
 	author = {Yang, Xuejun and Chen, Yang and Eide, Eric and Regehr, John},
-	title = {Finding and Understanding Bugs in C Compilers},
+	title = {Finding and Understanding Bugs in {C} Compilers},
 	booktitle = {Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design
                   and Implementation},
 	year = 2011,
@@ -506,7 +493,7 @@
 
 @inproceedings{blazy05_formal_verif_memor_model_c,
 	author = "Blazy, Sandrine and Leroy, Xavier",
-	title = "Formal Verification of a Memory Model for C-Like Imperative
+	title = "Formal Verification of a Memory Model for {C}-Like Imperative
                   Languages",
 	tags = {verification},
 	booktitle = "Formal Methods and Software Engineering",
@@ -520,7 +507,7 @@
 
 @inproceedings{slind08_brief_overv_hol4,
   author          = "Slind, Konrad and Norrish, Michael",
-  title           = "A Brief Overview of HOL4",
+  title           = "A Brief Overview of {HOL4}",
   booktitle       = "Theorem Proving in Higher Order Logics",
   year            = 2008,
   pages           = "28--32",
@@ -530,3 +517,51 @@
   keywords        = {theorem proving;HOL},
   publisher       = "Springer Berlin Heidelberg",
 }
+
+@inproceedings{meredith10_veril,
+	author = {P. {Meredith} and M. {Katelman} and J. {Meseguer} and
+                  G. {Ro{\c{s}}u}},
+	title = {A formal executable semantics of {Verilog}},
+	tags = {semantics},
+	booktitle = {Eighth ACM/IEEE International Conference on Formal Methods and
+                  Models for Codesign (MEMOCODE 2010)},
+	year = 2010,
+	pages = {179-188},
+	doi = {10.1109/MEMCOD.2010.5558634},
+	url = {https://doi.org/10.1109/MEMCOD.2010.5558634},
+	month = {July}
+}
+
+@inproceedings{jourdan12_valid_lr_parser,
+	author = "Jourdan, Jacques-Henri and Pottier, Fran{\c{c}}ois and
+                  Leroy, Xavier",
+	title = "Validating LR(1) Parsers",
+	booktitle = "Programming Languages and Systems",
+	year = 2012,
+	pages = "397--416",
+	address = "Berlin, Heidelberg",
+	editor = "Seidl, Helmut",
+	isbn = "978-3-642-28869-2",
+	publisher = "Springer Berlin Heidelberg"
+}
+
+@article{zhao12_formal_llvm_inter_repres_verif_progr_trans,
+  author          = {Zhao, Jianzhou and Nagarakatte, Santosh and Martin, Milo M.K. and Zdancewic,
+                  Steve},
+  title           = {Formalizing the {LLVM} Intermediate Representation for Verified Program
+                  Transformations},
+  journal         = {SIGPLAN Not.},
+  volume          = {47},
+  number          = {1},
+  pages           = {427-440},
+  year            = {2012},
+  doi             = {10.1145/2103621.2103709},
+  url             = {https://doi.org/10.1145/2103621.2103709},
+  address         = {New York, NY, USA},
+  issn            = {0362-1340},
+  issue_date      = {January 2012},
+  keywords        = {LLVM, memory safety, Coq},
+  month           = jan,
+  numpages        = {14},
+  publisher       = {Association for Computing Machinery},
+}