Distributing the Workload in a Lazy Theorem-Prover

Automated theorem proving consists in automatically (i.e. without any user interaction) discharging proof obligations which arise when applying rigorous methodologies for designing critical software systems. Recent developements in the so-called lazy approach in the integration of Boolean satisfiability with decision procedures for decidable theories of first-order logic have provided new means to efficiently prove or refute such proof obligations. In this paper, we present the first (known) attempt to design a distributed version of lazy theorem proving on a network of computers so that the available processing power can be used more effectively and avoid that automated reasoning be the bottleneck of the application of formal methods. Experiments clearly show the viability and the benefits of the proposed approach. © 2007 Elsevier B.V. All rights reserved.