Accession Number:

ADA459092

Title:

Parallel Randomized State-Space Search

Descriptive Note:

Corporate Author:

NEBRASKA UNIV LINCOLN DEPT OF COMPUTER SCIENCE AND ENGINEERING

Report Date:

2006-01-01

Pagination or Media Count:

11.0

Abstract:

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

Subject Categories:

  • Cybernetics
  • Economics and Cost Analysis

Distribution Statement:

APPROVED FOR PUBLIC RELEASE