Nuno P. Lopes,

Inesc-ID –

Abstract:

In this talk it will be presented a predicate abstraction and refinement-based algorithm for software verification that is designed for the distributed execution on compute nodes that communicate via message passing, as found in today's computer clusters. A successful adaptation of predicate abstraction and refinement from sequential to distributed setting needs to address challenges imposed by the inherent non-determinism present in distributed computing environments. In fact, our experiments show that up to an order of magnitude variation of the running time is common when a naive distribution scheme is applied, often resulting in significantly worse running time than the non-distributed version. It will be presented an algorithm that overcomes this pitfall by making deterministic the counterexample selection in spite of the distribution, and still efficiently exploits distributed computational resources. Joint work with Andrey Rybalchenko (TU Munich).

More info

Seminars page of INESC-ID
Seminar organized by the
ALGOS group (algos.inesc-id.pt)

 

Date: 2010-Sep-29     Time: 13:30:00     Room: 336

For more information: