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.
CITATION STYLE
Goel, A., & Sakallah, K. (2020). AVR: Abstractly verifying reachability. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 12078 LNCS, pp. 413–422). Springer. https://doi.org/10.1007/978-3-030-45190-5_23
Mendeley helps you to discover research relevant for your work.