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

    Nguyen, V. Y., & Ruys, T. C. (2008). Incremental Hashing for SPIN. In K. Havelund, R. Majumdar, & J. Palsberg (Eds.), Model Checking Software, Proceedings of the 15th International SPIN Workshop (pp. 232-249). [10.1007/978-3-540-85114-1_17] (Lecture Notes in Computer Science; Vol. 5156, No. WoTUG-31). Berlin: Springer. https://doi.org/10.1007/978-3-540-85114-1_17
    Nguyen, V.Y. ; Ruys, T.C. / Incremental Hashing for SPIN. Model Checking Software, Proceedings of the 15th International SPIN Workshop. editor / K. Havelund ; R. Majumdar ; J. Palsberg. Berlin : Springer, 2008. pp. 232-249 (Lecture Notes in Computer Science; WoTUG-31).
    @inproceedings{e6ebf741f8f54119a6d1707ebc258c2f,
    title = "Incremental Hashing for SPIN",
    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.",
    keywords = "FMT-MC: MODEL CHECKING, IR-62585, METIS-254957, EWI-14529",
    author = "V.Y. Nguyen and T.C. Ruys",
    note = "10.1007/978-3-540-85114-1_17",
    year = "2008",
    month = "8",
    doi = "10.1007/978-3-540-85114-1_17",
    language = "Undefined",
    isbn = "978-3-540-85113-4",
    series = "Lecture Notes in Computer Science",
    publisher = "Springer",
    number = "WoTUG-31",
    pages = "232--249",
    editor = "K. Havelund and R. Majumdar and J. Palsberg",
    booktitle = "Model Checking Software, Proceedings of the 15th International SPIN Workshop",

    }

    Nguyen, VY & Ruys, TC 2008, Incremental Hashing for SPIN. in K Havelund, R Majumdar & J Palsberg (eds), Model Checking Software, Proceedings of the 15th International SPIN Workshop., 10.1007/978-3-540-85114-1_17, Lecture Notes in Computer Science, no. WoTUG-31, vol. 5156, Springer, Berlin, pp. 232-249, 15th International SPIN Workshop on Model Checking Software 2008, Los Angeles, United States, 10/08/08. https://doi.org/10.1007/978-3-540-85114-1_17

    Incremental Hashing for SPIN. / Nguyen, V.Y.; Ruys, T.C.

    Model Checking Software, Proceedings of the 15th International SPIN Workshop. ed. / K. Havelund; R. Majumdar; J. Palsberg. Berlin : Springer, 2008. p. 232-249 10.1007/978-3-540-85114-1_17 (Lecture Notes in Computer Science; Vol. 5156, No. WoTUG-31).

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

    TY - GEN

    T1 - Incremental Hashing for SPIN

    AU - Nguyen, V.Y.

    AU - Ruys, T.C.

    N1 - 10.1007/978-3-540-85114-1_17

    PY - 2008/8

    Y1 - 2008/8

    N2 - 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.

    AB - 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.

    KW - FMT-MC: MODEL CHECKING

    KW - IR-62585

    KW - METIS-254957

    KW - EWI-14529

    U2 - 10.1007/978-3-540-85114-1_17

    DO - 10.1007/978-3-540-85114-1_17

    M3 - Conference contribution

    SN - 978-3-540-85113-4

    T3 - Lecture Notes in Computer Science

    SP - 232

    EP - 249

    BT - Model Checking Software, Proceedings of the 15th International SPIN Workshop

    A2 - Havelund, K.

    A2 - Majumdar, R.

    A2 - Palsberg, J.

    PB - Springer

    CY - Berlin

    ER -

    Nguyen VY, Ruys TC. Incremental Hashing for SPIN. In Havelund K, Majumdar R, Palsberg J, editors, Model Checking Software, Proceedings of the 15th International SPIN Workshop. Berlin: Springer. 2008. p. 232-249. 10.1007/978-3-540-85114-1_17. (Lecture Notes in Computer Science; WoTUG-31). https://doi.org/10.1007/978-3-540-85114-1_17