[Axiom-developer] LLVM to ACL2 translator

[Tim Daly]

This is exciting! 

Hardin, David S; Davis, Jennifer A.; Greve, David A.; McClurg, Dedidiah R.
"Development of a Translator from LLVM to ACL2"
Proc ACL2 (2014) pp163-177
http://arxiv.org/pdf/1406.1566v1

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 subsystems whose top-level assurance
relies on the assurance of the individual components. We have thus
undertaken a project to build a translator from LLVM to the applicative
subset of Common Lisp accepted by the ACL2 theorem prover. Our
translator produces executable ACL2 formal models, allowing us to both
prove theorems about the translated models as well as validate those
models by testing. The resulting models can be translated and certified
without user intervention, even for code with loops, thanks to the use
of the def::ung macro which allows us to defer the question of
termination. Initial measurements of concrete execution for translated
LLVM functions indicate that performance is nearly 2.4 million LLVM
instructions per second on a typical laptop computer.  In this paper we
overview the translation process and illustrate the translators's
capabilities by way of a concrete example, including both a functional
correctness theorem as well as a validation test for that example.