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.

Full Paper and Presentation

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


   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},

vv-lab/parallel-search-for-ltl-violations.txt · Last modified: 2015/02/18 19:49 by egm
Back to top
CC Attribution-Share Alike 4.0 International
chimeric.de = chi`s home Valid CSS Driven by DokuWiki do yourself a favour and use a real browser - get firefox!! Recent changes RSS feed Valid XHTML 1.0