2015/09/18 by David S. Hardin, David Hardin · 1 voice
Computer Science · #Automated theorem proving #Code (set theory) #Computer science #Executable #Interpreter #Logic, programming, and type systems #Parallel Computing and Optimization Techniques #Programming language #Set (abstract data type) #Software Testing and Debugging Techniques #Theoretical computer science #cs.LO #cs.PL
paper · pdf · doi:10.4204/eptcs.192.7
published as EPTCS 192, 2015, pp. 79-92 · In Proceedings ACL2 2015, arXiv:1509.05526
openalex publication_date 2015/09/18 · arxiv created 2015/09/21 · arxiv updated 2015/09/22 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/05
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 reported on a translator from LLVM to the applicative subset of Common Lisp accepted by the ACL2 theorem prover, producing executable ACL2 formal models, and allowing us to both prove theorems about the translated models as well as validate those models by testing. That translator provided many of the benefits of a pure decompilation into logic approach, but had the disadvantage of not being verified. The availability of Codewalker as of ACL2 7.0 has provided an opportunity to revisit this idea, and employ a more trustworthy decompilation into logic tool. Thus, we have employed the Codewalker method to create an interpreter for a subset of the LLVM instruction set, and have used Codewalker to analyze some simple array-based C programs compiled to LLVM form. We discuss advantages and limitations of the Codewalker-based method compared to the previous method, and provide some challenge problems for future Codewalker development.