@incollection{goelAVRAbstractlyVerifying2020,
 title = {{{AVR}}: {{Abstractly Verifying Reachability}}},
 author = {Goel, Aman and Sakallah, Karem},
 date = {2020},
 isbn = {978-3-030-45189-9 978-3-030-45190-5},
 doi = {10.1007/978-3-030-45190-5_23},
 url = {http://link.springer.com/10.1007/978-3-030-45190-5_23},
 urldate = {2023-01-10},
 booktitle = {Tools and {{Algorithms}} for the {{Construction}} and {{Analysis}} of {{Systems}}},
 editor = {Biere, Armin and Parker, David},
 volume = {12078},
 pages = {413--422},
 publisher = {Springer International Publishing},
 langid = {english},
 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.},
 location = {Cham},
 shorttitle = {{{AVR}}}
}