5 citations · 16 across the 6 of their papers we have counts for
6 papers
Hardware/Software Co-Assurance using the Rust Programming Language and ACL2
David Hardin
The Rust programming language has garnered significant interest and use as a modern, type-safe, memory-safe, and potentially formally analyzable programming language. Our interest…
Using ACL2 in the Design of Efficient, Verifiable Data Structures for High-Assurance Systems
David Hardin, Konrad Slind
Verification of algorithms and data structures utilized in modern autonomous and semi-autonomous vehicles for land, sea, air, and space presents a significant challenge. Autonomy a…
Reasoning About LLVM Code Using Codewalker
David S. Hardin
This paper reports on initial experiments using J Moore's Codewalker to reason about programs compiled to the Low-Level Virtual Machine (LLVM) intermediate form. Previously, we rep…
Development of a Translator from LLVM to ACL2
David S. Hardin, Jennifer A. Davis, David A. Greve +1
In our current work a library of formally verified software components is to be created, and assembled, using the Low-Level Virtual Machine (LLVM) intermediate form, into subsystem…
ACL2 Meets the GPU: Formalizing a CUDA-based Parallelizable All-Pairs Shortest Path Algorithm in ACL2
David S. Hardin, Samuel S. Hardin
As Graphics Processing Units (GPUs) have gained in capability and GPU development environments have matured, developers are increasingly turning to the GPU to off-load the main hos…
Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications
David Hardin, Julien Schmaltz
This volume contains the proceedings of ACL2 2011, the International Workshop on the ACL2 Theorem Prover and its Applications. The workshop was held in Austin, Texas, USA, on Novem…