Accession Number:

ADA416504

Title:

Report of the Project for Mechanizing Arithmetic

Descriptive Note:

Final rept. 15 Sep 2000-31 May 2003

Corporate Author:

TEXAS UNIV AT AUSTIN

Report Date:

2003-06-03

Pagination or Media Count:

116.0

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 Destinys XML output and converts it to ACL2.

Subject Categories:

  • Numerical Mathematics
  • Computer Programming and Software

Distribution Statement:

APPROVED FOR PUBLIC RELEASE