Abstract
PV (Protocol Veri.er) is an explicit enumeration based modelchecker for verifying finite state systems for next-time free LTL (LTL-X) properties. It implements a new partial order reduction algorithm, called Two-phase, that works in conjunction with selective caching to combat the state explosion problem faced by model-checkers.
Supported in part by ARPA Order #B990 Under SPAWAR Contract #N0039-95-C-018 (Avalanche), DARPA under contract #DABT6396C0094 (UV), and NSF MIP MIP-9321836.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
William R. Bryg, Kenneth K. Chan, and Nicholas S. Fiduccia. A high-performance, low-cost multiprocessor bus for workstations and midrange servers. Hewlett-Packard Journal, pages 18–24, February 1996.
John B. Carter, Chen-Chi Kuo, and Ravindra Kuramkote. A comparison of software and hardware synchronization mechanisms for distributed shared memory multiprocessors. Technical Report UUCS-96-011, University of Utah, Salt Lake City, UT, USA, September 1996.
W. W. Collier. Reasoning About Parallel Architectures. Prentice-Hall, Englewood Cliffs, NJ, 1992.
C. Courcoubetis, M. Vardi, P. Wolper, and M. Yannakakis. Memory efficient algorithms for the verification of temporal properties. In Computer Aided Verification, pages 233–242, June 1990.
G. Gopalakrishnan, R. Ghughal, R. Hosabettu, A. Mokkedem, and R. Nalumasu. Formal modeling and validation applied to a commercial coherent bus: A case study. In Hon F. Li and David K. Probst, editors, CHARME, Montreal, Canada, 1997.
Gerard Holzmann. Design and Validation of Computer Protocols. Prentice Hall, 1991.
Gerard Holzmann and Doron Peled. An improvement in formal verification. In Proceedings of Formal Description Techniques, Bern, Switzerland, October 1994.
Gerard J. Holzmann and Doron Peled. The state of Spin. In Rajeev Alur and Thomas A. Henzinger, editors, Computer Aided Verification, volume 1102 of Lecture Notes in Computer Science, pages 385–389, New Brunswick, New Jersey, July 1996. Springer-Verlag. Tool demo.
Ratan Nalumasu and Ganesh Gopalakrishnan. A partial order reduction algorithm without the proviso. Technical Report UUCS-98-017, University of Utah, Salt Lake City, UT, USA, August 1998.
Doron Peled. Combining partial order reductions with on-the-fly model-checking. Journal of Formal Methods in Systems Design, 8(1):39–64, 1996. also in Computer Aided Verification, 1994.
R. Tarjan. Depth-first search and linear graph algorithms. SIAM Journal on Computing, 1(2):146–160, June 1972.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nalumasu, R., Gopalakrishnan, G. (1998). PV: An Explicit Enumeration Model-Checker. In: Gopalakrishnan, G., Windley, P. (eds) Formal Methods in Computer-Aided Design. FMCAD 1998. Lecture Notes in Computer Science, vol 1522. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49519-3_35
Download citation
DOI: https://doi.org/10.1007/3-540-49519-3_35
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-65191-8
Online ISBN: 978-3-540-49519-2
eBook Packages: Springer Book Archive