AVR: Abstractly Verifying Reachability
Aman Goel
(
)
and Karem Sakallah
University of Michigan, Ann Arbor MI 48105, USA
{amangoel,karem}@umich.edu
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.
1 Introduction
Model checking [27,28] techniques based on incremental induction (like IC3
[19,31]) have gained significant success [21] due to their property-directed nature and clever use of incremental SAT solving. Bit-level implementations of IC3,
however, struggle with scalability due to being overwhelmed by low-level propositional learning [33]. Rapid advances in SMT solving [54,12] offer a solution and
allow for performing IC3 directly at the word level by combining the incremental
induction algorithm with an abstraction-refinement procedure [18,41,23,34].
AVR [2] is a model checker designed, primarily, for verifying safety properties
of hardware. It uses syntax-guided abstraction [34], a generalization of implicit
predicate abstraction [22], to perform IC3-style reachability on a first-order logic
encoding of the transition relation resulting in word-level clause learning. Upon
termination, AVR will either produce a proof certificate, in the form of a state
formula representing an inductive invariant, if the safety property holds or a
counterexample execution trace if it fails. In both cases, confidence in the verification output is achieved by using an external proof checker to independently
confirm the correctness of the proof certificate or a trace simulator depicting the
sequence of transitions leading to the failure. Beyond hardware, these features
allow AVR to be used in innovative ways including the verification of distributed
protocols defined over unbounded domains [44,45]. AVR also provides a variety of
complementary verification techniques, such as data abstraction and interpolation, to increase its scalability, as well as useful utilities, such as design statistics
and graphical visualizations, to provide high-level insights on the input design.
AVR was independently evaluated to be the best word-level verifier in the single
bit-vector track of Hardware Model Checking Competition (HWMCC) 2019 [17].
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 413–422, 2020.
https://doi.org/10.1007/978-3-030-45190-5 23
TACAS
Evaluation
Artifact
2020
Accepted
Aman Goel
(
)
and Karem Sakallah
University of Michigan, Ann Arbor MI 48105, USA
{amangoel,karem}@umich.edu
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.
1 Introduction
Model checking [27,28] techniques based on incremental induction (like IC3
[19,31]) have gained significant success [21] due to their property-directed nature and clever use of incremental SAT solving. Bit-level implementations of IC3,
however, struggle with scalability due to being overwhelmed by low-level propositional learning [33]. Rapid advances in SMT solving [54,12] offer a solution and
allow for performing IC3 directly at the word level by combining the incremental
induction algorithm with an abstraction-refinement procedure [18,41,23,34].
AVR [2] is a model checker designed, primarily, for verifying safety properties
of hardware. It uses syntax-guided abstraction [34], a generalization of implicit
predicate abstraction [22], to perform IC3-style reachability on a first-order logic
encoding of the transition relation resulting in word-level clause learning. Upon
termination, AVR will either produce a proof certificate, in the form of a state
formula representing an inductive invariant, if the safety property holds or a
counterexample execution trace if it fails. In both cases, confidence in the verification output is achieved by using an external proof checker to independently
confirm the correctness of the proof certificate or a trace simulator depicting the
sequence of transitions leading to the failure. Beyond hardware, these features
allow AVR to be used in innovative ways including the verification of distributed
protocols defined over unbounded domains [44,45]. AVR also provides a variety of
complementary verification techniques, such as data abstraction and interpolation, to increase its scalability, as well as useful utilities, such as design statistics
and graphical visualizations, to provide high-level insights on the input design.
AVR was independently evaluated to be the best word-level verifier in the single
bit-vector track of Hardware Model Checking Competition (HWMCC) 2019 [17].
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 413–422, 2020.
https://doi.org/10.1007/978-3-030-45190-5 23
TACAS
Evaluation
Artifact
2020
Accepted