Abstract
Thanks to a variety of new techniques, state-space exploration is becoming an increasingly effective method for the verification of concurrent programs. One of these techniques, hashing without collision detection, was proposed by Holzmann as a way to vastly reduce the amount of memory needed to store the explored state space. Unfortunately, this reduction in memory use comes at the price of a high probability of ignoring part of the state space and hence of missing existing errors. In this paper, we carefully analyze this method and show that, by using a modified strategy, it is possible to reduce the risk of error to a negligible amount while maintaining the memory use advantage of Holzmann's technique. Our proposed strategy has been implemented and we describe experiments that confirm the excellent expected results.
This work was supported by the Esprit BRA action REACT and by the Belgian Incentive Program “Information Technology” — Computer Science of the future, initiated by the Belgian State — Prime Minister's Office — Science Policy Office. The scientific responsability is assumed by its authors.
Chapter PDF
Similar content being viewed by others
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
S. Bensalem, A. Bouajjani, C. Loiseaux, and J. Sifakis. Property preserving simulations. In Proc. 4th Workshop on Computer Aided Verification, Montreal, June 1992.
M. Browne, E.M. Clarke, and D.L. Dill. Automatic circuit verification using temporal logic: Two new examples. In IEEE Int. Conf. on Computer Design: VLSI and Computers, Port Chester, October 1985.
E. M. Clarke, O. Grümberg, and D. E. Long. Model checking and abstraction. In Proc. 19th ACM Symposium on Principles of Programming Languages, pages 343–354, Albuquerque, New Mexico, January 1992.
C. Courcoubetis, M. Vardi, P. Wolper, and M. Yannakakis. Memory efficient algorithms for the verification of temporal properties. Formal Methods in System Design, 1:275–288, 1992.
J.C. Fernandez and L. Mounier. On the fly verification of behavioural equivalences and preorders. In Proc. 3rd Workshop on Computer Aided Verification, volume 575 of Lecture Notes in Computer Science, pages 181–191, Aalborg, July 1991.
P. Godefroid, G. J. Holzmann, and D. Pirottin. State space caching revisited. In Proc. 4th Workshop on Computer Aided Verification, Montreal, June 1992.
P. Godefroid and P. Wolper. A partial approach to model checking. In Proc. 6th Symp. on Logic in Computer Science, pages 406–415, Amsterdam, July 1991.
P. Godefroid and P. Wolper. Using partial orders for the efficient verification of deadlock freedom and safety properties. In Proc. 3rd Workshop on Computer Aided Verification, volume 575 of Lecture Notes in Computer Science, pages 332–342, Aalborg, July 1991. Springer-Verlag.
G. J. Holzmann, P. Godefroid, and D. Pirottin. Coverage preserving reduction strategies for reachability analysis. In Proc. 12th International Symposium on Protocol Specification, Testing, and Verification, Lake Buena Vista, Florida, June 1992. North-Holland.
G. J. Holzmann. Tracing protocols. AT&T Technical Journal, 64(12):2413–2434, 1985.
G. Holzmann. An improved protocol reachability analysis technique. Software Practice and Experience, 18(2):137–161, February 1988.
G. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall International Editions, 1991.
C. Jard and T. Jeron. On-line model-checking for finite linear temporal logic specifications. In Automatic Verification Methods for Finite State Systems, Proc. Int. Workshop, Grenoble, volume 407, pages 189–196, Grenoble, June 1989. Lecture Notes in Computer Science, Springer-Verlag.
K. McMillan. Using unfolding to avoid the state explosion problem in the verification of asynchronous circuits. In Proc. 4th Workshop on Computer Aided Verification, Montreal, June 1992.
J.L. Richier, C. Rodriguez, J. Sifakis, and J. Voiron. Verification in xesar of the sliding window protocol. In Proc. IFIP WG 6.1 7th Int. Conf. on Protocol Specification, Testing and Verification, pages 235–250, Zurich, 1987. North Holland.
A. Valmari. A stubborn attack on state explosion. In Proc. 2nd Workshop on Computer Aided Verification, volume 531 of Lecture Notes in Computer Science, pages 156–165, Rutgers, June 1990. Springer-Verlag.
M.Y. Vardi and P. Wolper. An automata-theoretic approach to automatic program verification. In Proc. Symp. on Logic in Computer Science, pages 322–331, Cambridge, June 1986.
P. Wolper. Expressing interesting properties of programs in propositional temporal logic. In Proc. 13th ACM Symp. on Principles of Programming, pages 184–192, St. Petersburgh, January 1986.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wolper, P., Leroy, D. (1993). Reliable hashing without collision detection. In: Courcoubetis, C. (eds) Computer Aided Verification. CAV 1993. Lecture Notes in Computer Science, vol 697. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56922-7_6
Download citation
DOI: https://doi.org/10.1007/3-540-56922-7_6
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56922-0
Online ISBN: 978-3-540-47787-7
eBook Packages: Springer Book Archive