AVR: Abstractly Verifying Reachability
415
AVR core performs IC3 with syntax-guided abstraction (IC3+SA) and implements several verification techniques and utilities (detailed in §3.1, §3.2).
SMT solver backends use the latest versions of state-of-the-art SMT solvers
(Yices 2 [30], Boolector [50], MathSAT 5 [24] and Z3 [48]) to efficiently integrate
incremental solver reasoning with AVR core using a C++ interface.
Multi-engine wrapper allows for process-level parallelism by running multiple
instances of AVR in parallel using proof race (as elaborated later in §3.3).
3.1 Techniques
At its core, AVR implements a word-level IC3 procedure where terms in the
implicit syntax of the problem are used as building blocks to perform IC3-style
clause learning at the word level using SMT solving. The key differences between IC3+SA [34], as implemented in AVR, and bit-level IC3 [19,31] can be
summarized as follows:
– IC3+SA uses relations defined over syntax terms (referred as atoms) instead
of individual state bits to implicitly represent an abstract state space.
– SMT solving is used instead of propositional SAT solving for solver reasoning.
– Counterexample-guided abstraction refinement [25] is used to automatically
eliminate the spurious behavior in the syntactically abstracted domain by
identifying new terms from the proof of unsatisfiability [42].
Within the core IC3+SA framework, AVR implements several optimizations and
important features that are helpful in improving model checking performance.
Core features
– Pre-processor optimizations perform simple transformations to standardize
and optimize the input model extracted from different input formats.
– Incremental refinement performs abstract counterexample analysis in an incremental fashion by using single-step solver queries instead of conventional
multi-step path queries.
– Incremental caching allows caching frequently-used data structures to speed
up incremental SMT solving (at the cost of increasing memory usage).
– Multiple SMT backends allow configuring usage of different SMT solvers for
different kinds of SMT queries based on the type of query.
Add-on techniques
– Property-directed splitting breaks wide words at bit-field extraction and concatenation boundaries [10] in a property-directed manner.
– Data abstraction focuses on the control structure of the problem by combining IC3+SA with data abstraction which converts data operations to
uninterpreted functions [20,11,41],.
– Interpolation adds Craig interpolants [46] and incremental refinement to
extract new terms from a spurious abstract counterexample.
– Extract/Concat handler adds a novel dedicated engine to deal with lightweight interpretation of bit-field extraction and concatenation operations.
415
AVR core performs IC3 with syntax-guided abstraction (IC3+SA) and implements several verification techniques and utilities (detailed in §3.1, §3.2).
SMT solver backends use the latest versions of state-of-the-art SMT solvers
(Yices 2 [30], Boolector [50], MathSAT 5 [24] and Z3 [48]) to efficiently integrate
incremental solver reasoning with AVR core using a C++ interface.
Multi-engine wrapper allows for process-level parallelism by running multiple
instances of AVR in parallel using proof race (as elaborated later in §3.3).
3.1 Techniques
At its core, AVR implements a word-level IC3 procedure where terms in the
implicit syntax of the problem are used as building blocks to perform IC3-style
clause learning at the word level using SMT solving. The key differences between IC3+SA [34], as implemented in AVR, and bit-level IC3 [19,31] can be
summarized as follows:
– IC3+SA uses relations defined over syntax terms (referred as atoms) instead
of individual state bits to implicitly represent an abstract state space.
– SMT solving is used instead of propositional SAT solving for solver reasoning.
– Counterexample-guided abstraction refinement [25] is used to automatically
eliminate the spurious behavior in the syntactically abstracted domain by
identifying new terms from the proof of unsatisfiability [42].
Within the core IC3+SA framework, AVR implements several optimizations and
important features that are helpful in improving model checking performance.
Core features
– Pre-processor optimizations perform simple transformations to standardize
and optimize the input model extracted from different input formats.
– Incremental refinement performs abstract counterexample analysis in an incremental fashion by using single-step solver queries instead of conventional
multi-step path queries.
– Incremental caching allows caching frequently-used data structures to speed
up incremental SMT solving (at the cost of increasing memory usage).
– Multiple SMT backends allow configuring usage of different SMT solvers for
different kinds of SMT queries based on the type of query.
Add-on techniques
– Property-directed splitting breaks wide words at bit-field extraction and concatenation boundaries [10] in a property-directed manner.
– Data abstraction focuses on the control structure of the problem by combining IC3+SA with data abstraction which converts data operations to
uninterpreted functions [20,11,41],.
– Interpolation adds Craig interpolants [46] and incremental refinement to
extract new terms from a spurious abstract counterexample.
– Extract/Concat handler adds a novel dedicated engine to deal with lightweight interpretation of bit-field extraction and concatenation operations.