Report of the Project for Mechanizing Arithmetic
Abstract
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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jun 03, 2003
- Accession Number
- ADA416504
Entities
People
- J. S. Moore
- Jeff Golden
- Robert Krug
- Warren A. Hunt Jr.
Organizations
- University of Texas at Austin