User-friendly model checking: Automatically configuring algorithms with rulebase/PE

Abstract

Model checking is known to be computationally hard, meaning no single algorithm can efficiently solve all problems. A possible approach is to run many algorithms in parallel until one of themfinds a solution. This approach is sometimes called state-of-the-art (SOTA) model checker. However, hardware resources are often limited, forcing some selection. In this paper we present an automatic decision system, called Whisperer, which generates an optimized set of configured algorithms for a given model-checking problem. The system weights the advice of advisors, each predicting the fitness of a different algorithm for the problem. Advisors also monitor the progress of currently running algorithms, allowing the replacement of ineffective algorithms. Whisperer is built into the formal verification platform, RuleBase/PE, and allows novice users to skip the delicate task of algorithm selection. Our experiments showWhisperer, after some training, performs nearly as well as SOTA. © Springer-Verlag Berlin Heidelberg 2009.