Advertisement

A theory of generic interpreters

  • Phillip J. Windley
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 683)

Abstract

We present an abstract theory of interpreters. Interpreters are models of computation that are specifically designed for use as templates in computer system specification and verification. The generic interpreter theory contains an abstract representation which serves as an interface to the theory and as a guide to specification. A set of theory obligations ensure that the theory is being used correctly and provide a guide to system verification. The generic interpreter theory provides a methodology for deriving important definitions and lemmas that were previously obtained in a largely ad hoc fashion. Many of the complex data and temporal abstractions are done in the abstract theory and need not be redone when the theory is used.

Keywords

Composition Operator Abstract Theory Generic Interpreter State Stream Concrete Level 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

References

  1. [Aro90]
    Tejkumar Arora. The formal verification of the VIPER microprocessor: EBM to microcode level. Master's thesis, University of California, Davis, 1990.Google Scholar
  2. [Coe92]
    Michael L. Coe and Phillip J. Windley. Using the Generic Interpreter Theory to Verify Microprocessors: A Tutorial. Technical Report LAL-92-10, University of Idaho, Department of Computer Science, Laboratory for Applied Logic. December, 1992.Google Scholar
  3. [Coh88]
    Avra Cohn. Correctness properties of the VIPER block model: The second level. Technical Report 134, University of Cambridge Computer Laboratory, May 1988.Google Scholar
  4. [SRI88]
    SRI International Computer Science Laboratory. EHDM Specification and Verification System: User's Guide, Version 4.1.1988.Google Scholar
  5. [Gor88]
    Michael J.C. Gordon. HOL: A proof generating system for higher-order logic. In G. Birtwhistle and P.A Subrahmanyam, editors, VLSI Specification,Verification, and Synthesis. Kluwer Academic Press, 1988.Google Scholar
  6. [Gog88]
    J. Goguen and T. Winkler. Introducing OBJ3. Technical Report SRI-CSL-88-9, SRI International, August 1988.Google Scholar
  7. [Her88]
    John Herbert. Temporal abstraction of digital designs. In G.J. Milne, editor, The Fusion of Hardware Design and Verification, Proceedings of the IFIP WG 10.2 International Working Conference, Glasgow, Scotland. North-Holland, 1988.Google Scholar
  8. [Hun87]
    Warren A. Hunt. The mechanical verification of a microprocessor design. In D. Borrione, editor, From HDL Descriptions to Guaranteed Correct Circuit Designs. Elsevier Scientific Publishers, 1987.Google Scholar
  9. [Hun89]
    Warren A. Hunt. Microprocessor design verification. Journal of Automated Reasoning, Vol 5, pages 429–460,1989.Google Scholar
  10. [Joy89]
    Jeffrey J. Joyce. Multi-Level Verification of Microprocessor-Based Systems. PhD thesis, Cambridge University, December 1989.Google Scholar
  11. [Low89]
    Paul Loewenstein. Reasoning about state machines in higher-order logic. In M. Leeser and G. Brown, editors, Workshop on Hardware Specification, Verification, and Synthesis: Mathematical Aspects, Lecture Notes in Computer Science. Springer-Verlag, 1989.Google Scholar
  12. [Mel88]
    Thomas Melham. Abstraction mechanisms for hardware verification. In G. Birtwhistle and P. A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis. Kluwer Academic Publishers, 1988.Google Scholar
  13. [Win90a]
    Phillip J. Windley. The Formal Verification of Generic Interpreters. PhD thesis, University of California, Davis, Division of Computer Science, June 1990.Google Scholar
  14. [Win90b]
    Phillip J. Windley. A hierarchical methodology for the verification of microprogrammed microprocessors. In Proceedings of the IEEE Symposium on Security and Privacy, May 1990.Google Scholar
  15. [Win91]
    Phillip J. Windley. The formal specification of a high-speed CMOS correlator. In Proceedings of the Third Annual IEEE/NASA Symposium on VLSI Design, October 1991.Google Scholar
  16. [Win92]
    Phillip J. Windley. Abstract Theories in HOL. In Proceedings of the 1992 International Conference on the HOL theorem Prover and its Application, October 1992.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1993

Authors and Affiliations

  • Phillip J. Windley
    • 1
  1. 1.Laboratory for Applied Logic Department of Computer ScienceUniversity of IdahoMoscowUSA

Personalised recommendations