Verification of Year 2000 Conversion Rules

Matt Kaufmann
EDS CIO Services
March, 1999

Included here are the following documents underlying the paper "Verification of Year 2000 Conversion Rules Using the ACL2 Theorem Prover," to appear in Software Tools for Technology Transfer. Or, you can fetch them all at once: First save the gzipped tar file acl2-y2k.tar.gz. Then in a Unix shell execute these commands

gunzip acl2-y2k.tar.gz
tar xvfp acl2-y2k.tar
in order to get these files in a new directory called acl2-y2k/.

README high-level instructions
apply-rules.lisp code for printing dates.out from dates.lisp
dates-sample.lisp rules, proofs, and documentation
dates-sample.out rules report
makefile for running ACL2 and re-making output files
print-rules.lisp top-level input file