Report of the Project for Mechanizing Arithmetic
Final rept. 15 Sep 2000-31 May 2003
TEXAS UNIV AT AUSTIN
Pagination or Media Count:
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 Destinys XML output and converts it to ACL2.
- Numerical Mathematics
- Computer Programming and Software