Parameterized verification of fault tolerant protocols

Staff - Faculty of Informatics

Start date: 19 May 2010

End date: 20 May 2010

The Faculty of Informatics is pleased to announce a seminar given by Francesco Alberti

DATE: Wednesday, May 19th, 2010
PLACE: USI Università della Svizzera italiana, room SI-004, Informatics building (Via G. Buffi 13)
TIME: 11.00

Automating the verification of fault tolerant protocols turns out to be a daunting task as  they are aften parametric, i.e. they are designed to work with an arbitrary finite number of processes. So, checking that a protocol satisfies a certain property requires to prove it regardless of the number of processes involved in its execution or, in other words, to perform a parameterized verification.
We propose a new approach to the parameterized verification of distributed and fault-tolerant systems by using a logical approach, implemented in a model checker called MCMT, that allows us to specify systems in a declarative way. To prove the practical viability of this approach, I applied it to formally check the agreement property of the reliable broadcast protocols of Chandra and Toueg.

I got my M.Sc. degree in Computer Science on April 26, 2010 at the Università degli Studi di Milano (University of Milan, Italy). My master thesis was about the (formal) parameterized verification of fault-tolerant protocols by using the SMT-based model checker MCMT.

HOST: prof. Natasha Sharygina