Parameterized verification of fault tolerant protocols
Decanato - Facoltà di scienze informatiche
Data d'inizio: 19 Maggio 2010
Data di fine: 20 Maggio 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
ABSTRACT:
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.
BIO:
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
