University of Twente Student Theses


Bit-packing and Hashing Evaluation in Explicit-state Model Checking

Hol, Valentijn (2022) Bit-packing and Hashing Evaluation in Explicit-state Model Checking.

[img] PDF
Abstract:MCSTA is a model checking tool for models written in the Modest language. It can be used to formally verify certain properties of a model. During model checking a model’s state space needs to be (exhaustively) explored which takes a significant amount of time and memory – depending on model complexity. This research evaluates the impact of bit-packing state member variables by examining the execution time and memory consumption. We find that in all cases there is a decrease in memory usage, and in most cases a minor decrease in execution time. Furthermore, we propose an algorithm for selective field unpacking, to improve the performance of bit-packing, whilst maintaining near-optimal state sizes. Lastly, we evaluate the current hash function used in state space exploration based on hash-table bucket lengths, and find it to be performing adequately with little room for improvement.
Item Type:Essay (Bachelor)
Faculty:EEMCS: Electrical Engineering, Mathematics and Computer Science
Subject:54 computer science
Programme:Computer Science BSc (56964)
Link to this item:
Export this item as:BibTeX
HTML Citation
Reference Manager


Repository Staff Only: item control page