Incremental Hashing for SPIN

Viet Yen Nguyen; Theo C. Ruys

doi:10.1007/978-3-540-85114-1_17

Incremental Hashing for SPIN

Viet Yen Nguyen, Theo C. Ruys

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

7 Citations (Scopus)

2 Downloads (Pure)

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 language	English
Title of host publication	Model Checking Software
Subtitle of host publication	15th International SPIN Workshop, Los Angeles, CA, USA, August 10-12, 2008, Proceedings
Editors	K. Havelund, R. Majumdar, J. Palsberg
Place of Publication	Berlin, Heidelberg
Publisher	Springer
Pages	232-249
Number of pages	18
ISBN (Electronic)	978-3-540-85114-1
ISBN (Print)	978-3-540-85113-4
DOIs	https://doi.org/10.1007/978-3-540-85114-1_17
Publication status	Published - Aug 2008
Event	15th International SPIN Workshop on Model Checking Software 2008 - Los Angeles, United States Duration: 10 Aug 2008 → 12 Aug 2008 Conference number: 15

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	5156
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Name	Theoretical Computer Science and General Issues
Publisher	Springer
ISSN (Print)	2512-2010
ISSN (Electronic)	2512-2029

Workshop

Workshop	15th International SPIN Workshop on Model Checking Software 2008
Country/Territory	United States
City	Los Angeles
Period	10/08/08 → 12/08/08

Keywords

FMT-MC: MODEL CHECKING
n/a OA procedure

Access to Document

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

Cite this

Nguyen, V. Y., & Ruys, T. C. (2008). Incremental Hashing for SPIN. In K. Havelund, R. Majumdar, & J. Palsberg (Eds.), Model Checking Software: 15th International SPIN Workshop, Los Angeles, CA, USA, August 10-12, 2008, Proceedings (pp. 232-249). (Lecture Notes in Computer Science; Vol. 5156), (Theoretical Computer Science and General Issues). Springer. https://doi.org/10.1007/978-3-540-85114-1_17

@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{\textquoteright}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{\textquoteright}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{\textquoteright}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, n/a OA procedure",

author = "Nguyen, {Viet Yen} and Ruys, {Theo C.}",

year = "2008",

month = aug,

doi = "10.1007/978-3-540-85114-1_17",

language = "English",

isbn = "978-3-540-85113-4",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "232--249",

editor = "K. Havelund and R. Majumdar and J. Palsberg",

booktitle = "Model Checking Software",

address = "Germany",

note = "15th International SPIN Workshop on Model Checking Software 2008 ; Conference date: 10-08-2008 Through 12-08-2008",

}

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

Incremental Hashing for SPIN. / Nguyen, Viet Yen; Ruys, Theo C.
Model Checking Software: 15th International SPIN Workshop, Los Angeles, CA, USA, August 10-12, 2008, Proceedings. ed. / K. Havelund; R. Majumdar; J. Palsberg. Berlin, Heidelberg: Springer, 2008. p. 232-249 (Lecture Notes in Computer Science; Vol. 5156), (Theoretical Computer Science and General Issues).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Incremental Hashing for SPIN

AU - Nguyen, Viet Yen

AU - Ruys, Theo C.

N1 - Conference code: 15

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 - n/a OA procedure

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

A2 - Havelund, K.

A2 - Majumdar, R.

A2 - Palsberg, J.

PB - Springer

CY - Berlin, Heidelberg

T2 - 15th International SPIN Workshop on Model Checking Software 2008

Y2 - 10 August 2008 through 12 August 2008

ER -

Nguyen VY, Ruys TC. Incremental Hashing for SPIN. In Havelund K, Majumdar R, Palsberg J, editors, Model Checking Software: 15th International SPIN Workshop, Los Angeles, CA, USA, August 10-12, 2008, Proceedings. Berlin, Heidelberg: Springer. 2008. p. 232-249. (Lecture Notes in Computer Science). (Theoretical Computer Science and General Issues). doi: 10.1007/978-3-540-85114-1_17

Incremental Hashing for SPIN

Abstract

Publication series

Workshop

Keywords

Access to Document

Fingerprint

Cite this