Advertisement

Verification of Year 2000 conversion rules using the ACL2 theorem prover

  • Matt Kaufmann
Special section an theorem proving
  • 17 Downloads

Abstract.

The well-publicized Year 2000 problem provides interesting challenges for the remediation of noncompliant code. This paper describes some work done at EDS CIO Services, using the ACL2 theorem prover to formally verify correctness of remediation rules. The rules take into account the possibility of “flag” (non-date) values of date variables. Many of them have been implemented in an in-house tool, COGEN 2000TM, that corrects for noncompliant date-related logic in COBOL programs.

Key words: Formal verification – Year 2000 – ACL2 – Automated reasoning – Program transformation 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Matt Kaufmann
    • 1
  1. 1.EDS CIO Services, 98 San Jacinto Blvd., Suite 500, Austin, TX 78701, USAUS

Personalised recommendations