@misc(RustAndroidArs,
 author       = {Ron Amadeo},
 year         = {2021},
 title        = {Google is now writing low-level {A}ndroid code in {R}ust},
 url          = {https://arstechnica.com/gadgets/2021/04/google-is-now-writing-low-level-android-code-in-rust/},
)
@inproceedings(Hatcliff2011,
 author       = {Jason Belt and John Hatcliff and Robby and Patrice Chalin and David S. Hardin and Xianghua Deng},
 year         = {2011},
 title        = {Bakar Kiasan: Flexible Contract Checking for Critical Systems using Symbolic Execution},
 booktitle    = {Proceedings of the Third NASA Formal Methods Symposium (NFM 2011)},
 pages        = {58--72},
 doi          = {10.1007/978-3-642-20398-5\_6},
)
@inproceedings(stobj,
 author       = {Robert S. Boyer and J Strother Moore},
 year         = {2002},
 title        = {Single-Threaded Objects in {ACL2}},
 booktitle    = {Practical Aspects of Declarative Languages, 4th International Symposium, {PADL} 2002, Portland, OR, USA, January 19-20, 2002, Proceedings},
 series       = {LNCS},
 volume       = {2257},
 publisher    = {Springer},
 pages        = {9--27},
 doi          = {10.1007/3-540-45587-6_3},
)
@book(feiler-AADL,
 author       = {Peter H. Feiler and David P. Gluch},
 year         = {2012},
 title        = {Model-Based Engineering with AADL: An Introduction to the SAE Architecture Analysis \& Design Language},
 edition      = {1st},
 publisher    = {Addison-Wesley Professional},
)
@inproceedings(arrayset-stobj,
 author       = {David S. Hardin},
 year         = {2013},
 title        = {The Specification, Verification, and Implementation of a High-Assurance Data Structure: An {ACL2} Approach},
 booktitle    = {Proceedings of the 46th Hawaii International Conference on System Sciences},
 pages        = {5059--5067},
 doi          = {10.1109/HICSS.2013.541},
)
@inproceedings(hardin-rac,
 author       = {David S. Hardin},
 year         = {2020},
 title        = {Put Me on the {RAC}},
 booktitle    = {Proceedings of the Sixteenth International Workshop on the {ACL2} Theorem Prover and its Applications (ACL2-20)},
 pages        = {142--145},
)
@inproceedings(hardin-co-assurance,
 author       = {David S. Hardin},
 year         = {2020},
 title        = {Verified Hardware/Software Co-Assurance: Enhancing Safety and Security for Critical Systems},
 booktitle    = {Proceedings of the 2020 {IEEE} Systems Conference},
 doi          = {10.1109/SysCon47679.2020.9381831},
)
@inproceedings(Hardin2009b,
 author       = {David S. Hardin and T. Douglas Hiratzka and D. Randolph Johnson and Lucas G. Wagner and Michael W. Whalen},
 year         = {2009},
 title        = {Development of Security Software: A High Assurance Methodology},
 editor       = {K. Breitman and A. Cavalcanti},
 booktitle    = {Proceedings of the 11th International Conference on Formal Engineering Methods (ICFEM'09)},
 publisher    = {Springer},
 pages        = {266--285},
 doi          = {10.1007/978-3-642-10373-5_14},
)
@inproceedings(formal-filter-synth-langsec,
 author       = {David S. Hardin and Konrad L. Slind},
 year         = {2021},
 title        = {Formal Synthesis of Filter Components for Use in Security-Enhancing Architectural Transformations},
 booktitle    = {Proceedings of the Seventh Workshop on Language-Theoretic Security, 42nd {IEEE} Symposium and Workshops on Security and Privacy ({L}ang{S}ec 2021)},
 doi          = {10.1109/SPW53761.2021.00024},
)
@book(Rust2018,
 author       = {Steve Klabnik and Carol Nichols},
 year         = {2018},
 title        = {The Rust Programming Language},
 publisher    = {No Starch Press},
)
@inproceedings(cakeml:popl14,
 author       = {Ramana Kumar and Magnus O. Myreen and Michael Norrish and Scott Owens},
 year         = {2014},
 title        = {{CakeML}: a verified implementation of {ML}},
 editor       = {Suresh Jagannathan and Peter Sewell},
 booktitle    = {The 41st Annual {ACM} {SIGPLAN-SIGACT} Symposium on Principles of Programming Languages, {POPL} '14, San Diego, CA, USA, January 20-21, 2014},
 publisher    = {{ACM}},
 pages        = {179--192},
 doi          = {10.1145/2535838.2535841},
)
@article(leroy:cacm,
 author       = {Xavier Leroy},
 year         = {2009},
 title        = {Formal verification of a realistic compiler},
 journal      = {Communications of the {ACM}},
 volume       = {52},
 number       = {7},
 pages        = {107--115},
 doi          = {10.1145/1538788.1538814},
)
@book(JVM,
 author       = {Tim Lindholm and Frank Yellin and Gilad Bracha and Alex Buckley},
 year         = {2013},
 title        = {The Java Virtual Machine Specification},
 publisher    = {Addison-Wesley},
)
@manual(LLVM,
 organization = {LLVM Project},
 year         = {2020},
 title        = {The {LLVM} Compiler Infrastructure},
 url          = {http://llvm.org/},
)
@manual(Simulink,
 organization = {The {M}ath{W}orks, Inc.},
 year         = {2020},
 title        = {Simulink},
 url          = {https://www.mathworks.com/products/simulink.html},
)
@manual(AlgoC,
 organization = {Mentor Graphics Corporation},
 year         = {2016},
 title        = {Algorithmic C (AC) Datatypes},
 url          = {https://www.mentor.com/hls-lp/downloads/ac-datatypes},
)
@manual(Catapult,
 organization = {Mentor Graphics Corporation},
 year         = {2020},
 title        = {Catapult High-Level Synthesis},
 url          = {https://www.mentor.com/hls-lp/catapult-high-level-synthesis/},
)
@inproceedings(case-models-2021,
 author       = {Eric Mercer and Konrad Slind and Isaac Amundson and Darren Cofer and Junaid Babar and David Hardin},
 year         = {2021},
 title        = {Synthesizing Verified Components for Cyber Assured Systems Engineering},
 booktitle    = {24th International Conference on Model-Driven Engineering Languages and Systems (MODELS 2021)},
 doi          = {10.1109/MODELS50736.2021.00029},
)
@misc(MSBugs,
 author       = {Matt Miller},
 year         = {2019},
 title        = {A proactive approach to more secure code},
 url          = {https://msrc-blog.microsoft.com/2019/07/16/a-proactive-approach-to-more-secure-code/},
)
@misc(SustainableRust,
 author       = {Shane Miller and Carl Lerche},
 year         = {2022},
 title        = {Sustainability with {R}ust},
 url          = {https://aws.amazon.com/blogs/opensource/sustainability-with-rust/},
)
@article(Gryphon:CACM,
 author       = {Steven Miller and Michael Whalen and Darren Cofer},
 year         = {2010},
 title        = {Software model checking takes off},
 journal      = {Communications of the {ACM}},
 volume       = {53},
 pages        = {58--64},
 doi          = {10.1145/1646353.1646372},
)
@phdthesis(myreen:phd,
 author       = {Magnus Myreen},
 year         = {2009},
 title        = {Formal verification of machine-code programs},
 school       = {University of Cambridge},
)
@article(HLS,
 author       = {Razvan Nane and Vlad-Mihai Sima and Christian Pilato and Jongsok Choi and Blair Fort and Andrew Canis and Yu Ting Chen and Hsuan Hsiao and Stephen Brown and Fabrizio Ferrandi and Jason Anderson and Koen Bertels},
 year         = {2016},
 title        = {A Survey and Evaluation of FPGA High-Level Synthesis Tools},
 journal      = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},
 volume       = {35},
 number       = {10},
 pages        = {1591--1604},
 doi          = {10.1109/TCAD.2015.2513673},
)
@inproceedings(EverParse,
 author       = {Tahina Ramananandro and Delignat-Lavaud, Antoine and Cedric Fournet and Nikhil Swamy and Tej Chajed and Nadim Kobeissi and Jonathan Protzenko},
 year         = {2019},
 title        = {Ever{P}arse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats},
 booktitle    = {{USENIX} Security \IeC{\textquoteleft}19},
)
@inproceedings(slang,
 author       = {Robby and John Hatcliff},
 year         = {2021},
 title        = {{Slang}: The {Sireum} Programming Language},
 booktitle    = {10th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation ({ISoLA})},
 series       = {LNCS},
 volume       = {13036},
 pages        = {253--273},
 doi          = {10.1007/978-3-030-89159-6_17},
)
@manual(DO-178C,
 organization = {{RTCA} {C}ommittee {SC}-205},
 year         = {2015},
 title        = {DO-178C Software Considerations in Airborne Systems and Equipment Certification},
 url          = {https://my.rtca.org/nc\_\_store?search=DO-178C},
)
@book(Russinoff2022,
 author       = {David M. Russinoff},
 year         = {2022},
 title        = {Formal Verification of Floating-Point Hardware Design: A Mathematical Approach},
 edition      = {second},
 publisher    = {Springer},
 doi          = {10.1007/978-3-030-87181-9},
)
@manual(plex,
 author       = {Geoffry Song},
 year         = {2020},
 title        = {plex: a parser and lexer generator as a {R}ust procedural macro},
 url          = {https://github.com/goffrie/plex},
)
@misc(RustAndroid,
 author       = {Jeff Vander Stoep and Stephen Hines},
 year         = {2021},
 title        = {Rust in the {A}ndroid platform},
 url          = {https://security.googleblog.com/2021/04/rust-in-android-platform.html},
)
@manual(monocypher,
 author       = {Loup Vaillant},
 year         = {2022},
 title        = {Monocypher: Boring Crypto that Simply Works},
 url          = {https://monocypher.org},
)
@manual(VivadoHLS,
 organization = {Xilinx, Inc.},
 year         = {2018},
 title        = {Vivado Design Suite User Guide: High-Level Synthesis},
 url          = {https://www.xilinx.com/support/documentation/sw_manuals/xilinx2018_3/ug902-vivado-high-level-synthesis.pdf},
)
@inproceedings(CUnusable,
 author       = {Victor Yodaiken},
 year         = {2021},
 title        = {How {ISO C} became unusable for operating systems development},
 booktitle    = {Proceedings of the 11th Workshop on Programming Languages and Operating Systems},
 pages        = {84--90},
 doi          = {10.1145/3477113.3487274},
)