mcmillanDeductiveVerificationDecidable2018:
  type: anthos
  title: Deductive {Verification} in {Decidable Fragments} with {Ivy}
  author:
  - McMillan, Kenneth L.
  - Padon, Oded
  date: 2018
  editor: Podelski, Andreas
  page-range: 43-55
  url:
    value: http://link.springer.com/10.1007/978-3-319-99725-4_4
    date: 2023-02-07
  serial-number:
    doi: 10.1007/978-3-319-99725-4_4
    isbn: 978-3-319-99724-7 978-3-319-99725-4
  language: en-US
  abstract: This paper surveys the work to date on Ivy, a language and a tool for the formal specification and verification of distributed systems. Ivy supports deductive verification using automated provers, model checking, automated testing, manual theorem proving and generation of executable code. In order to achieve greater verification productivity, a key design goal for Ivy is to allow the engineer to apply automated provers in the realm in which their performance is relatively predictable, stable and transparent. In particular Ivy focuses on the use of decidable fragments of first-order logic. We consider the rationale or Ivy’s design, the various capabilities of the tool, as well as case studies and applications.
  parent:
    type: anthology
    title: Static {Analysis}
    publisher:
      name: Springer International Publishing
      location: Cham
    volume: 11002