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.
Distributing the Workload in a Lazy Theorem-Prover / Deharbe, D.; Ranise, S.; Vidal, J.. - In: ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE. - ISSN 1571-0661. - 184:SPEC. ISS.(2007), pp. 21-37. [10.1016/j.entcs.2007.03.013]
Distributing the Workload in a Lazy Theorem-Prover
Ranise S.;
2007-01-01
Abstract
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.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione