On Symmetry and Quantification: A New Approach to Verify Distributed Protocols
Channel: Aman Goel
Date: 2021-04-29

Paper by Aman Goel (https://aman-goel.github.io) and Karem Sakallah (https://web.eecs.umich.edu/~karem) from the University of Michigan (https://umich.edu), presented at the 13th NASA Formal Methods Symposium (NFM) 2021 (https://shemesh.larc.nasa.gov/nfm2021)

Presents IC3PO: IC3 for Proving Protocol Properties, a tool for verifying distributed protocols fully automatically

Checkout IC3PO on GitHub - https://github.com/aman-goel/ic3po
Extended paper on arXiv - https://arxiv.org/abs/2103.14831

Time-stamps:
0:00 Introduction
00:21 Multi-signature smart contract
00:58 Why verify
02:06 IC3PO preview
02:50 IC3PO's key ingredients
03:47 Model Checking & AVR
06:07 Verifying distributed protocols
06:51 IC3PO at a high level
09:46​ Symmetry-aware clause boosting
15:13​ Finite-domain inductive invariant
18:07 IC3PO summary
18:37 Evaluation
23:09 Summary