Abstract

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.