Mechanizing Arithmetic II (CD-ROM)
Golden, Jeff, Warren A. Hunt, Robert Bellarmine Krug, J. S. Moore · Defense Technical Information Center (DTIC) · 2003
ELECTRONIC FILE CHARACTERISTICS: 2,093 files; PostScript (.PS) and HyperText Markup Language (.HTML). See supplementary note for more information. PHYSICAL DESCRIPTION: 1 computer laser optical disc (CD-ROM); 4 3/4 in.; 36.4 MB. SYSTEMS DETAIL NOTE: IBM-clone PC-compatible. 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.