Put Me on the RAC

D. Hardin

Sixteenth International Workshop on the ACL2 Theorem Prover and its Applications (ACL2'20), May 2020

We have a keen research interest in Hardware/Software Co-Assurance. This interest is motivated in part by emerging application areas, such as autonomous and semi-autonomous platforms for land, sea, air, and space, that require sophisticated algorithms and data structures, are subject to stringent accreditation/certification, and encourage hardware/software co-design approaches. As part of our research, we have conducted several experiments employing a state-of-the-art toolchain, due to Russinoff and O’Leary, and originally designed for use in floating-point hardware verification, to determine its suitability for the creation of various safety-critical/security-critical applications in numerous domains.