418
A. Goel and K. Sakallah
generally expressed over unbounded domains (with an unbounded number of
clients, servers, epochs, messages, etc.). The I4 system [45,44] demonstrates how
AVR can be used to verify a simpler finite version of the protocol, followed by
generalizing AVR’s proof certificates to the unbounded domain. For example, a
finite-domain invariant saying “clients C 1 and C 2 cannot both link to the server
S” i.e. ¬(link(C 1 , S) ∧ link(C 2 , S)) can be generalized to the unbounded domain
as “no two different clients can both link to a server” i.e.
∀ C1,C2,S (C 1 = C 2 ) =⇒ ¬(link(C 1 , S) ∧ link(C 2 , S)).
5 Strengths
Control-centric properties, where much of the complexity lies in the control logic
(such as sequential equivalence checking, microprocessor instruction control unit,
key-value store) are much easier to verify using AVR. Syntax-guided abstraction
hides the domain complexity outside of the problem syntax, and automatically
separates important control-flow details from the irrelevant data component.
This, combined with data abstraction, allows for scalable model checking with
the capacity to scale independently of the variable bit widths [33,34].
Push-button verification using AVR eliminates the need for tedious human intervention in verification (such as manual identification of abstraction predicates,
manually adding helper assertions) by automatic incremental construction of
abstraction and word-level clauses using the IC3+SA algorithm.
Provable assurance on the verification outcome is guaranteed by AVR using
independently-checkable proof certificates and counterexample traces.
Useful utilities that AVR provides, such as support for multiple input formats,
efficient integration with state-of-the-art SMT solvers, proof race, high-level system statistics, graphical visualizations, etc. contribute to a user-friendly experience and ease of use.
6 Limitations
Heavy data dependency can make word-level techniques in AVR ineffective for
certain problems, especially when a majority of bit-precise values in the data
domain play an important role (for example, puzzle solving problems like Tower
of Hanoi [39], Peg Solitaire [38], etc. formulated as reachability problems [52]).
Logic synthesis and bit-level optimizations [14,47] can be very useful for such
problems and help bit-level checkers perform better than word-level techniques
by significantly decreasing the problem complexity at the bit level.
First-order logic fragments beyond quantifier-free bit-vectors, arrays and uninterpreted functions (such as non-linear arithmetic, floating-point numbers, quantifiers, etc.) and properties beyond safety (such as liveness and fairness) have
limited support in the current tool implementation. AVR’s primary focus has
been on verification of safety properties defined on hardware systems.
A. Goel and K. Sakallah
generally expressed over unbounded domains (with an unbounded number of
clients, servers, epochs, messages, etc.). The I4 system [45,44] demonstrates how
AVR can be used to verify a simpler finite version of the protocol, followed by
generalizing AVR’s proof certificates to the unbounded domain. For example, a
finite-domain invariant saying “clients C 1 and C 2 cannot both link to the server
S” i.e. ¬(link(C 1 , S) ∧ link(C 2 , S)) can be generalized to the unbounded domain
as “no two different clients can both link to a server” i.e.
∀ C1,C2,S (C 1 = C 2 ) =⇒ ¬(link(C 1 , S) ∧ link(C 2 , S)).
5 Strengths
Control-centric properties, where much of the complexity lies in the control logic
(such as sequential equivalence checking, microprocessor instruction control unit,
key-value store) are much easier to verify using AVR. Syntax-guided abstraction
hides the domain complexity outside of the problem syntax, and automatically
separates important control-flow details from the irrelevant data component.
This, combined with data abstraction, allows for scalable model checking with
the capacity to scale independently of the variable bit widths [33,34].
Push-button verification using AVR eliminates the need for tedious human intervention in verification (such as manual identification of abstraction predicates,
manually adding helper assertions) by automatic incremental construction of
abstraction and word-level clauses using the IC3+SA algorithm.
Provable assurance on the verification outcome is guaranteed by AVR using
independently-checkable proof certificates and counterexample traces.
Useful utilities that AVR provides, such as support for multiple input formats,
efficient integration with state-of-the-art SMT solvers, proof race, high-level system statistics, graphical visualizations, etc. contribute to a user-friendly experience and ease of use.
6 Limitations
Heavy data dependency can make word-level techniques in AVR ineffective for
certain problems, especially when a majority of bit-precise values in the data
domain play an important role (for example, puzzle solving problems like Tower
of Hanoi [39], Peg Solitaire [38], etc. formulated as reachability problems [52]).
Logic synthesis and bit-level optimizations [14,47] can be very useful for such
problems and help bit-level checkers perform better than word-level techniques
by significantly decreasing the problem complexity at the bit level.
First-order logic fragments beyond quantifier-free bit-vectors, arrays and uninterpreted functions (such as non-linear arithmetic, floating-point numbers, quantifiers, etc.) and properties beyond safety (such as liveness and fairness) have
limited support in the current tool implementation. AVR’s primary focus has
been on verification of safety properties defined on hardware systems.