Personal tools
You are here: Home Events Abstract Archives 2000 Verification of broadcast protocols

Verification of broadcast protocols

Javier Esparza Technical University of Munich 4pm, Friday 3 November 2000 Room 2511, JCMB, King's Buildings

Broadcast protocols model parameterised systems in which a finite but arbitrarily large number of identical processes communicate. Communication takes place by means of rendez-vous (two processes exchange a message) or broadcasts (a process sends a message to all the others). A protocol satisfies a property if the property holds for any number of processes. Most model checking techniques cannot be applied to this problem, because they can only prove the property for a fixed (and usually small) number of processes.

In the talk I introduce a constraint programming approach to the verification of safety properties. I briefly discuss basic theory, algorithms, efficient data structures, and case studies in the area of cache coherence protocols.

Document Actions