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.tarin 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 |