References

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