Report of the Project for Mechanizing Arithmetic
Golden, Jeff, Warren A. Hunt, Robert Bellarmine Krug, J. S. Moore · Defense Technical Information Center (DTIC) · 2003
The primary goal of this project has been to improve the degree of automation in the ACL2 when proving theorems about computer programs. We have paid particular attention to fixed-width integer arithmetic and the Java Virtual Machine (JVM). Our work has proceeded on three fronts. We have begun developing an approach for automating much of the detail work involved in applying the ACL2 method for proving theorems about low-level programs. Work completed includes a prototype tool targeting the language of the JVM, and a preliminary JVM-specific lemma library designed to facilitate reasoning about refined JVM models. We have improved the ACL2 theorem prover itself. We have also developed an improved library of arithmetic lemmas. We have begun work in cooperation with the Destiny Project. Destiny is an automated program verifier under development by the government. We have developed a first version of a tool that reads Destiny's XML output and converts it to ACL2.