Date: Wed 15 Dec 1999
Time: 15.00
Place: Aula 214

Speaker: Giorgio Delzanno
Title: Constraint-based Analysis of Broadcast Protocols
(joint work with Javier Esparza and Andreas Podelski)

Abstract. Broadcast protocols are systems composed of a finite but arbitrarily large number of processes that communicate by rendezvous (two processes exchange a message) or by broadcast (a process sends a message to all other processes). In the talk we discuss an optimized algorithm for the automatic verification of safety properties in broadcast protocols. The algorithm checks whether a property holds for any number of processes. The representation of sets of states is given through a special class of linear arithmetic constraints.