Explicit State Model Checking with Hopper

The Murϕ-based Hopper tool is a general purpose explicit model checker. Hopper leverages Murϕ’s class structure to implement new algorithms. Hopper differs from Murϕ in that it includes in its distribution published parallel and disk based algorithms, as well as several new algorithms. For example, Hopper includes parallel dynamic partitioning, cooperative parallel search for LTL violations and property-based guided search (parallel or sequential). We discuss Hopper in general and present a recently implemented randomized guided search algorithm. In multiple parallel guided searches, randomization increases the expected average time to find an error but decreases the expected minimum time to find an error. The Hopper1 tool leverages the Murϕ architecture to implement parallel, disk-based and heuristic model checking algorithms. The common theme in the algorithms implemented in Hopper is that they do not use abstraction. Instead, Hopper explores fundamental algorithms for reduci...

• Type: Conference
• Year: 2004
• Where: SPIN
• Authors: Michael Jones, Eric Mercer
• Keywords: Algorithm, Disk Based Algorithms, Hopper Leverages Murϕ, SPIN 2004, Theoretical Computer Science