maI4IncrementalInference2019:
  type: article
  title:
    value: 'I4: Incremental Inference of Inductive Invariants for Verification of Distributed Protocols'
    short: I4
  author:
  - Ma, Haojun
  - Goel, Aman
  - Jeannin, Jean-Baptiste
  - Kapritsos, Manos
  - Kasikci, Baris
  - Sakallah, Karem A.
  date: 2019-10-27
  page-range: 370-384
  url:
    value: https://dl.acm.org/doi/10.1145/3341301.3359651
    date: 2023-01-10
  serial-number:
    doi: 10.1145/3341301.3359651
    isbn: 978-1-4503-6873-5
  language: en-US
  abstract: 'Designing and implementing distributed systems correctly is a very challenging task. Recently, formal verification has been successfully used to prove the correctness of distributed systems. At the heart of formal verification lies a computerchecked proof with an inductive invariant. Finding this inductive invariant, however, is the most difficult part of the proof. Alas, current proof techniques require inductive invariants to be found manually—and painstakingly—by the developer. In this paper, we present a new approach, Incremental Inference of Inductive Invariants (I4), to automatically generate inductive invariants for distributed protocols. The essence of our idea is simple: the inductive invariant of a finite instance of the protocol can be used to infer a general inductive invariant for the infinite distributed protocol. In I4, we create a finite instance of the protocol; use a model checking tool to automatically derive the inductive invariant for this finite instance; and generalize this invariant to an inductive invariant for the infinite protocol. Our experiments show that I4 can prove the correctness of several distributed protocols like Chord, 2PC and Transaction Chains with little to no human effort.'
  parent:
  - type: proceedings
    title: Proceedings of the 27th {ACM Symposium} on {Operating Systems Principles}
    publisher:
      name: ACM
      location: Huntsville Ontario Canada
  - type: conference
    title: '{SOSP} ''19: {ACM SIGOPS} 27th {Symposium} on {Operating Systems Principles}'