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…