Incremental Hashing for SPIN

V.Y. Nguyen, T.C. Ruys

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    6 Citations (Scopus)

    Abstract

    This paper discusses a generalised incremental hashing scheme for explicit state model checkers. The hashing scheme has been implemented into the model checker Spin. The incremental hashing scheme works for Spin’s exhaustive and both approximate verification modes: bitstate hashing and hash compaction. An implementation is provided for 32-bit and 64-bit architectures. We performed extensive experiments on the BEEM benchmarks to compare the incremental hash functions against Spin’s traditional hash functions. In almost all cases, incremental hashing is faster than traditional hashing. The amount of performance gain depends on several factors, though. We conclude that incremental hashing performs best for the (64-bits) Spin’s bitstate hashing mode, on models with large state vectors, and using a verifier, that is optimised by the C compiler.
    Original languageUndefined
    Title of host publicationModel Checking Software, Proceedings of the 15th International SPIN Workshop
    EditorsK. Havelund, R. Majumdar, J. Palsberg
    Place of PublicationBerlin
    PublisherSpringer
    Pages232-249
    Number of pages18
    ISBN (Print)978-3-540-85113-4
    DOIs
    Publication statusPublished - Aug 2008
    Event15th International SPIN Workshop on Model Checking Software 2008 - Los Angeles, United States
    Duration: 10 Aug 200812 Aug 2008
    Conference number: 15

    Publication series

    NameLecture Notes in Computer Science
    PublisherSpringer Verlag
    NumberWoTUG-31
    Volume5156

    Workshop

    Workshop15th International SPIN Workshop on Model Checking Software 2008
    CountryUnited States
    CityLos Angeles
    Period10/08/0812/08/08

    Keywords

    • FMT-MC: MODEL CHECKING
    • IR-62585
    • METIS-254957
    • EWI-14529

    Cite this