PV1 Peregrineverifies that a population protocol computes a user-specified predicate

Tool for the analysis and parameterized verification of population protocols

Application domain/field

Type of tool

Analysis tool

Expected input

Population protocol


Graphical editor or Python script

Expected output

Depends on the option chosen to analyse a protocol. For verification it will show whether correctness could be proven or not. If not, then it can give a counterexample.


Peregrine has several options for analysing a protocol, including: A protocol computes a predicate φ if, for every initial configuration C, all fair executions from C lead to a lasting consensus φ(C){0,1}. Uses Z3 to check satisfiability of Presburger arithmetic formulas.


On scalability of Peregrine (from the CAV 2018 paper): "Currently, Peregrine can verify protocols with up to a hundred states and a few thousands transitions. The bottleneck is the size of the constraint system."
Protocol Simulation


Related papers

Peregrine: A Tool for the Analysis of Population Protocols

Last publication date

18 July 2018

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.