Parallel Randomized State-Space Search

摘要: Model checkers search the space of possible program behaviors to detect errors and demonstrate their absence. Despite major advances in reduction optimization techniques, state-space can still become cost-prohibitive as size complexity increase. In this paper, we present a technique for dramatically improving cost- effectiveness techniques error detection using parallelism. Our approach be composed with all are aware amplify benefits. It was developed based on insights gained from performing large empirical study cost-effectiveness randomization analysis. We explain those our technique, then show through focused that speeds up analysis by factors ranging 2 over 1000 compared traditional modes search, does so relatively small numbers parallel processors.