The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.10 - October (2007 vol.33)
pp: 659-674
ABSTRACT
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.
INDEX TERMS
Software/Program Verification, Model Checking, Models of Computation, Logics and meanings of Programs, Distributed Programming
CITATION
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
34 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool