Population protocols (Angluin et al., PODC 2004) are a formal model of sensor networks consisting of identical, finite-state mobile devices. When two devices come into the range of each other, they interact and change their state. Computations are infinite sequences of pairwise interactions where the interacting processes are picked by a fair scheduler.

A population protocol is well specified if for every initial configuration of devices, and for every fair computation starting at it, all devices eventually agree on a consensus value that only depends on the initial configuration. If a protocol is well specified, then it is said to compute the predicate that assigns to each initial configuration its consensus value.

In the talk I will report on our recent results on automatic verification of population protocols: Is a given protocol well specified? Does a given protocol compute a given predicate? Does it compute it within a given time? These questions require to check liveness properties of parameterized systems with an arbitrary number of agents, and are very challenging. I show how to attack them using the theory of Vector Addition Systems and SMT technology.