Abstract
This paper presents work directed toward making the Nuprl interactive theorem prover a more effective tool for protocol verification while retaining existing advantages of the system, and describes application of the prover to verifying the SCI cache coherence protocol. The verification is based, in part, on formal mathematics imported from another theorem-proving system, exploiting a connection we implemented between Nuprl and HOL. We have designed and implemented a type annotation scheme for Nuprl's logic that allows type information to be effectively applied by the system's automated reasoning facilities. This is significant because Nuprl's powerful constructive type theory buys much of its expressive power and flexibility at the cost of giving up the more manageable kinds of type system found in other logics.
Chapter PDF
Keywords
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
C.-T. Chou and D. Peled. Verifying a model-checking algorithm. In Tools and Algorithms for the Construction and Analysis of Systems, volume 1055 of Lecture Notes in Computer Science, pages 241–257. Springer-Verlag, 1996.
R. L. Constable, et al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs, New Jersey, 1986.
A. Felty and F. Stomp. A correctness proof of a cache coherence protocol. 1997. Available at www.cs.bell-labs.com/~felty/sci/. An earlier version appears in Proceedings of the 11th Annual Conference on Computer Assurance, 1996.
A. P. Felty and D. J. Howe. Hybrid interactive theorem proving using Nuprl and HOL. In Fourteenth International Conference on Automated Deduction, volume 1249 of Lecture Notes in Computer Science, pages 351–365. Springer-Verlag, 1997.
M. J. C. Gordon and T. F. Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993.
D. J. Howe. On computational open-endedness in Martin-Löf's type theory. In Proceedings of the Sixth Annual Symposium on Logic in Computer Science, pages 162–172. IEEE Computer Society, 1991.
D. J. Howe. Importing mathematics from HOL into Nuprl. In Theorem Proving in Higher Order Logics, volume 1125 of Lecture Notes in Computer Science, pages 267–281. Springer-Verlag, 1996.
IEEE-P1596-05Nov90-docl97-iii. Part INA: SCI Coherence Overview, 1990. Unapproved Draft. Approved standard is described in IEEE Std. 1596–1992 “The Scalable Coherent Interface”.
S. Owre and N. Shankar. The formal semantics of PVS. Technical report, SRI, August 1997.
S. Park and D. L. Dill. Verification of FLASH cache coherence protocol by aggregation of distributed transactions. In 8th ACM Symposium on Parallel Algorithms and Architectures, 1996.
U. Stern and D. L. Dill. Automatic verification of the SCI cache coherence protocol. In Correct Hardware Design and Verification Methods, 1995.
B. Werner. Sets in types, types in sets. In International Symposium on Theoretical Aspects of Computer Software, volume 1281 of Lecture Notes in Computer Science. Springer-Verlag, 1997.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Felty, A.P., Howe, D.J., Stomp, F.A. (1998). Protocol verification in Nuprl. In: Hu, A.J., Vardi, M.Y. (eds) Computer Aided Verification. CAV 1998. Lecture Notes in Computer Science, vol 1427. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0028764
Download citation
DOI: https://doi.org/10.1007/BFb0028764
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64608-2
Online ISBN: 978-3-540-69339-0
eBook Packages: Springer Book Archive