Recent advances in parallel model checking for liveness properties achieve significant capacity increases over sequential model checkers. However, the capacity of parallel model checkers is in turn limited by available aggregate memory and network bandwidth. We propose a new parallel algorithm that sacrifices complete coverage for increased capacity to find errors. The algorithm, called BEE (for bee-based error exploration) uses coordinated depth-bounded random walks to reduce memory and bandwidth demands. A unique advantage of BEE is that it is well-suited for use on clusters of non-dedicated workstations.

PDF Version or access through the ACM Portal.

Jones, M. D. and Sorber, J. 2005. Parallel search for LTL violations. Int. J. Softw. Tools Technol. Transf. 7, 1 (Feb. 2005), 31-42. DOI= http://dx.doi.org/10.1007/s10009-003-0115-8

@article{1045583,
   author = {Jones,, Michael D. and Sorber,, Jacob},
   title = {Parallel search for LTL violations},
   journal = {Int. J. Softw. Tools Technol. Transf.},
   volume = {7},
   number = {1},
   year = {2005},
   issn = {1433-2779},
   pages = {31--42},
   doi = {http://dx.doi.org/10.1007/s10009-003-0115-8},
   publisher = {Springer-Verlag},
   address = {Berlin, Heidelberg},
}