goelAVRAbstractlyVerifying2020:
  type: anthos
  title:
    value: '{AVR}: {Abstractly Verifying Reachability}'
    short: '{AVR}'
  author:
  - Goel, Aman
  - Sakallah, Karem
  date: 2020
  editor:
  - Biere, Armin
  - Parker, David
  page-range: 413-422
  url:
    value: http://link.springer.com/10.1007/978-3-030-45190-5_23
    date: 2023-01-10
  serial-number:
    doi: 10.1007/978-3-030-45190-5_23
    isbn: 978-3-030-45189-9 978-3-030-45190-5
  language: en-US
  abstract: We present AVR, a push-button model checker for verifying state transition systems directly at the source-code level. AVR uses information embedded in the word-level syntax of the design representation to automatically perform scalable model checking by combining a novel syntax-guided abstraction-refinement technique with a word-level implementation of the IC3 algorithm. AVR provides independently-verifiable certificates that offer provable assurance and are easy to relate to the word-level system. Moreover, proof certificates can be further used in innovative ways to extract key design information and are useful in a growing number of applications.
  parent:
    type: anthology
    title: Tools and {Algorithms} for the {Construction} and {Analysis} of {Systems}
    publisher:
      name: Springer International Publishing
      location: Cham
    volume: 12078