Issue No.10 - October (2007 vol.33)
We describe an extension of the SPIN model checker for use on multi-core shared-memory systems and report on its performance. We show how, with proper load balancing, the time requirements of a verification run can in some cases be reduced close to N-fold when N processing cores are used. We also analyze the types of verification problems for which multi-core algorithms cannot provide relief. The extensions discussed here require only relatively small changes in the SPIN source code, and are compatible with most existing verification modes, such as partial order reduction, the verification of temporal logic formulae, bitstate hashing, and hash-compact compression.
Software/Program Verification, Model Checking, Models of Computation, Logics and meanings of Programs, Distributed Programming
Gerard J. Holzmann, Dragan Bosnacki, "The Design of a Multicore Extension of the SPIN Model Checker", IEEE Transactions on Software Engineering, vol.33, no. 10, pp. 659-674, October 2007, doi:10.1109/TSE.2007.70724