  Proving that an unbounded distributed protocol satisfies a given safety
property amounts to finding a quantified inductive invariant that implies the
property for all possible instance sizes of the protocol. Existing methods for
solving this problem can be described as search procedures for an invariant
whose quantification prefix fits a particular template. We propose an
alternative constructive approach that does not prescribe, a priori, a specific
quantifier prefix. Instead, the required prefix is automatically inferred
without any search by carefully analyzing the structural symmetries of the
protocol. The key insight underlying this approach is that symmetry and
quantification are closely related concepts that express protocol invariance
under different re-arrangements of its components. We propose symmetric
incremental induction, an extension of the finite-domain IC3/PDR algorithm,
that automatically derives the required quantified inductive invariant by
exploiting the connection between symmetry and quantification. While various
attempts have been made to exploit symmetry in verification applications, to
our knowledge, this is the first demonstration of a direct link between
symmetry and quantification in the context of clause learning during
incremental induction. We also describe a procedure to automatically find a
minimal finite size, the cutoff, that yields a quantified invariant proving
safety for any size.
  Our approach is implemented in IC3PO, a new verifier for distributed
protocols that significantly outperforms the state-of-the-art, scales orders of
magnitude faster, and robustly derives compact inductive invariants fully
automatically.
