SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
  SRI Logo

Systematic Formal Verification of Interpreters
 by Dr. John Rushby, David Cyrluk & Mandayam Srivas.

From First International Conference on Formal Engineering Methods (ICFEM '97).
Edited by Michael G. Hinchey and Shaoying Liu.
IEEE Computer Society, Hiroshima, Japan.
November, 1997.
Pages 140–149.

Formal methods have gained acceptance in the hardware field through a pragmatic approach that has succeeded in providing systematic, scalable, highly automated, and cost-effective treatments for certain stereotypical problems of practical importance. By identifying stereotypical problems, the effort required to develop effective formal methods has been amortized over many applications. We suggest that formal methods can achieve similar industrial success in selected software applications by following the same principles. As illustration, we examine approaches to the stereotypical problem of interpreter correctness in the presence of timing differences between the specification and implementation interpreters. In hardware, this corresponds to the problem of verifying microprogrammed, pipelined, or superscalar processors, but it has wider applications to any system--hardware or software--that can be considered as an interpreter.
BibTEX Entry
    AUTHOR = {David Cyrluk and John Rushby and Mandayam Srivas},
    TITLE = {Systematic Formal Verification of Interpreters},
    BOOKTITLE = {First International Conference on Formal Engineering Methods (ICFEM '97)},
    YEAR = {1997},
    EDITOR = {Michael {G.} Hinchey and Shaoying Liu},
    PAGES = {140--149},
    ADDRESS = {Hiroshima, Japan},
    MONTH = {nov},
    ORGANIZATION = {{IEEE} Computer Society},
    URL = {}


About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2024 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy