Name
Abstract | ||
|---|---|---|
We present a new version of Peregrine, the tool for the analysis and parameterized verification of population protocols introduced in [Blondin et al., CAV'2018]. Population protocols are a model of computation, intensely studied by the distributed computing community, in which mobile anonymous agents interact stochastically to perform a task. Peregrine 2.0 features a novel verification engine based on the construction of stage graphs. Stage graphs are proof certificates, introduced in [Blondin et al., CAV'2020], that are typically succinct and can be independently checked. Moreover, unlike the techniques of Peregrine 1.0, the stage graph methodology can verify protocols whose executions never terminate, a class including recent fast majority protocols. Peregrine 2.0 also features a novel proof visualization component that allows the user to interactively explore the stage graph generated for a given protocol. |
Year | DOI | Venue |
|---|---|---|
2020 | 10.1007/978-3-030-59152-6_32 | ATVA |
DocType | Citations | PageRank |
Conference | 0 | 0.34 |
References | Authors | |
0 | 4 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Javier Esparza | 1 | 770 | 60.33 |
| Martin Helfrich | 2 | 0 | 0.68 |
| Stefan Jaax | 3 | 10 | 1.51 |
| Philipp Meyer | 4 | 29 | 4.72 |