Parallel search for LTL violations

Michael D. Jones and Jacob Sorber

From the issue entitled "Special section on parallel and distributed model checking"

View Related Documents

Abstract

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 nondedicated workstations.

Keywords  Semiformal verification - Explicit model checking - Biologically inspired algorithms

Fulltext Preview

Image of the first page of the fulltext document