mcmillanIvyMultimodalVerification2020:
  type: anthos
  title:
    value: 'Ivy: {A Multi-modal Verification Tool} for {Distributed Algorithms}'
    short: Ivy
  author:
  - McMillan, Kenneth L.
  - Padon, Oded
  date: 2020
  editor:
  - Lahiri, Shuvendu K.
  - Wang, Chao
  page-range: 190-202
  url:
    value: http://link.springer.com/10.1007/978-3-030-53291-8_12
    date: 2023-02-07
  serial-number:
    doi: 10.1007/978-3-030-53291-8_12
    isbn: 978-3-030-53290-1 978-3-030-53291-8
  language: en-US
  abstract: 'Ivy is a multi-modal verification tool for correct design and implementation of distributed protocols and algorithms, supporting modular specification, implementation and proof. Ivy supports proving safety and liveness properties of parameterized and infinite-state systems via three modes: deductive verification using an SMT solver, abstraction and model checking, and manual proofs using natural deduction. It supports light-weight formal methods via compositional specification-based testing and bounded model checking. Ivy can extract executable distributed programs by translation to efficient C++ code. It is designed to support decidable automated reasoning, to improve proof stability and to provide transparency in the case of proof failures. For this purpose, it presents concrete finite counterexamples, automatically audits proofs for decidability of verification conditions, and provides modular hiding of theories.'
  parent:
    type: anthology
    title: Computer {Aided Verification}
    publisher:
      name: Springer International Publishing
      location: Cham
    volume: 12225