@incollection{goelSymmetryQuantificationNew2021,
 title = {On {{Symmetry}} and {{Quantification}}: {{A New Approach}} to {{Verify Distributed Protocols}}},
 author = {Goel, Aman and Sakallah, Karem A.},
 date = {2021},
 doi = {10.1007/978-3-030-76384-8_9},
 url = {http://arxiv.org/abs/2103.14831},
 urldate = {2023-01-10},
 volume = {12673},
 pages = {131--150},
 keywords = {Computer Science - Distributed Parallel and Cluster Computing,Computer Science - Formal Languages and Automata Theory,Computer Science - Logic in Computer Science},
 abstract = {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.},
 eprintclass = {cs},
 eprinttype = {arXiv},
 eprint = {2103.14831},
 shorttitle = {On {{Symmetry}} and {{Quantification}}},
 booktitle = {NASA Formal Methods (NFM 2021)},
 series = {Lecture Notes in Computer Science}
}

goelSymmetryQuantificationNew2021:
  type: anthos
  title:
    value: 'On {Symmetry} and {Quantification}: {A New Approach} to {Verify Distributed Protocols}'
    short: On {Symmetry} and {Quantification}
  author:
  - Goel, Aman
  - Sakallah, Karem A.
  date: 2021
  page-range: 131-150
  url:
    value: http://arxiv.org/abs/2103.14831
    date: 2023-01-10
  serial-number:
    arxiv: '2103.14831'
    doi: 10.1007/978-3-030-76384-8_9
  abstract: 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.
  parent:
    type: anthology
    title: NASA Formal Methods (NFM 2021)
    volume: 12673
    parent:
      type: anthology
      title: Lecture Notes in Computer Science