diff options
Diffstat (limited to 'references.bib')
-rw-r--r-- | references.bib | 69 |
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}, +} |