Abstract
The bitstate hashing, or supertrace, technique was introduced in 1987 as a method to increase the quality of verification by reachability analyses for applications that defeat analysis by traditional means because of their size. Since then, the technique has been included in many research verification tools, and was even adopted in some tools that are marketed commercially. It is therefore important that we understand well how and why the method works, what its limitations are, and how it compares with alternative schemes that attempt to solve the same problem.
The original motivation for the bitstate hashing technique was based on empirical evidence of its effectiveness. In this paper we provide the analytical argument. We compare the technique with two alternatives that have been proposed in the recent literature as potential improvements.
Chapter PDF
Similar content being viewed by others
References
Cattel, T. (1994) ‘Modelization and verification of a multiprocessor realtime OS kernel,’ Proc. 7th FORTE Conference, Bern, Switzerland, pp. 35–51.
Chaves, J. (1991) ‘Formal methods at ATamp;T, an industrial usage report,’ Proc. 4th FORTE Conference, Sydney, Australia, pp. 83–90.
Godefroid, P., Holzmann, G.J., and Pirottin, D. (1992) ‘State space caching revisited,’ Proc. 4th Int. Conference on Computer Aided Verification, Montreal, Canada, LNCS Vol. 663, pp. 178–191.
Holzmann, G.J. (1987) ‘On limits and possibilities of automated protocol analysis,’ Proc. 7th IFIP WG 6.1 Int. Workshop on Protocol Specification, Testing, and Verification, North-Holland Publ., Amsterdam, pp. 137–161.
Holzmann, G.J. (1988) ‘An improved protocol reachability analysis technique,’ Software, Practice and Experience, Vol. 18, No. 2, pp. 137–161.
Holzmann, G J (1991) Design and validation of computer protocols, Prentice Hall, Englewood Cliffs, NJ.
Holzmann, G.J., Godefroid, P., and Pirottin, D. (1992) ‘Coverage preserving reduction strategies for reachability analysis,’ Proc. 12th IFIP WG 6.1 Int. Workshop on Protocol Specification, Testing, and Verification, North-Holland Publ., Amsterdam, pp. 349–363.
Holzmann, G.J. (1994) ‘The theory and practice of a formal method: NewCoRe,’ Proc. 13th IFIP World Computer Congress, Hamburg, Germany.
Holzmann, G.J. (1994) ‘Proving the value of formal methods,’ Proc. 7th FORTE Conference, Bern, Switzerland, Chapman amp; Hall, pp. 385–396.
Lin, F.J. (1994) ‘Specification and validation of communications in client/server models,’ Proc. 1994 Int. Conference on Network Protocols ICNP, Boston, Mass., pp. 108–116.
Stern, U., and Dill, D. (1995) ‘Improved probabilistic verification by hash compaction,’ Report Stanford University, submitted for publication.
Wolper, P. and Leroy, D. (1993) ‘Reliable hashing without collision detection,’ Proc. 5th Int. Conference on Computer Aided Verification, Elounda, Greece, pp. 59–70.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1996 IFIP International Federation for Information Processing
About this chapter
Cite this chapter
Holzmann, G.J. (1996). An analysis of bitstate hashing. In: Dembiński, P., Średniawa, M. (eds) Protocol Specification, Testing and Verification XV. PSTV 1995. IFIP Advances in Information and Communication Technology. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-34892-6_19
Download citation
DOI: https://doi.org/10.1007/978-0-387-34892-6_19
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-5041-2925-1
Online ISBN: 978-0-387-34892-6
eBook Packages: Springer Book Archive