Population Protocols: Beyond Runtime Analysis

I survey our recent work on the verification of population protocols and their state complexity.