Advertisement

Problems encountered in the machine-assisted proof of hardware

  • Paul Curzon
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 987)

Abstract

We describe our experiences verifying real communications hardware using machine-assisted proof. In particular we reflect on the errors found, problems encountered and the bottlenecks that slowed the progress of the proofs. We also note techniques which would alleviate the problems. Most of the problems we discuss only become significant when large designs are verified.

Keywords

Asynchronous Transfer Mode Formal Verification Proof Obligation Proof Assistant Switching Element 
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. 1.
    Paul Curzon. Experiences formally verifying a network component. In Proceedings of the 9th Annual IEEE Conference on Computer Assurance, pages 183–193. IEEE Press, 1994.Google Scholar
  2. 2.
    Paul Curzon. The formal verification of the Fairisle ATM switching element. Technical Report 329, University of Cambridge Computer Laboratory, March 1994.Google Scholar
  3. 3.
    Paul Curzon. Tracking design changes with formal machine-checked proof. The Computer Journal, 38(2), 1995.Google Scholar
  4. 4.
    Paul Curzon. Virtual theories. In Proceedings of the 8th International Workshop on Higher Order Logic Theorem Proving and Its Applications, Lecture Notes in Computer Science. Springer-Verlag, 1995.Google Scholar
  5. 5.
    M.J.C. Gordon and T.F. Melham. Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, 1993.Google Scholar
  6. 6.
    F.K. Hanna and N. Daeche. Dependent types and formal synthesis. In C. A. R. Hoare and M. J. C. Gordon, editors, Mechanized Reasoning and Hardware Design, pages 49–68. Prentice Hall, 1992.Google Scholar
  7. 7.
    I.M. Leslie and D.R. McAuley. Fairisle: An ATM network for the local area. ACM Communication Review, 19(4):327–336, September 1991.Google Scholar
  8. 8.
    Donald Syme. A new interface for HOL — ideas, issues and implementation. In Proceedings of the 8th International Workshop on Higher Order Logic Theorem Proving and Its Applications, Lecture Notes in Computer Science. Springer-Verlag, 1995.Google Scholar
  9. 9.
    P.J. Windley, K. Levitt, and G.C. Cohen. The formal verification of generic interpreters. Technical Report 4403, NASA Contractor Report, October 1991.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Paul Curzon
    • 1
  1. 1.University of Cambridge Computer LaboratoryCambridgeUK

Personalised recommendations