416
A. Goel and K. Sakallah
– Bounded model checking (BMC) [15] allows for an alternative to the IC3+SA
engine for quick bug hunting, especially for shallow bugs.
– Other options include adding global assumptions lazily, minimizing proof
certificates, making syntax-guided abstraction closer to (resp. farther from)
implicit predicate abstraction by decreasing (resp. increasing) abstraction
granularity, exploiting randomness during solving, and a few others.
Utilities
AVR also provides a number of useful utilities to the user including:
– Printing the problem in SMT-LIB format [13].
– Graphical visualizations of the problem and the word-level clause learning.
– Detailed statistics report on the input design and the verification run.
3.2 Certificates
Once a model checking problem is solved, there can be two possible outcomes:
either the property holds (safe), or it fails (unsafe).
If the property holds, IC3+SA produces an inductive invariant, i.e. an approximate fixpoint that establishes the property to be true in all executions of
the system. Inductive invariants act as proof certificates that guarantee the correctness of the verification outcome. AVR prints such proof certificates directly in
the SMT-LIB format, which allows for independent checking of their correctness
using an external SMT solver like Yices 2 or Z3. Since proof certificates are in
the word-level format, they are human-readable and much easier to relate to the
word-level input directly at the source-code level (as against bit-level invariants
which are usually too hard to understand). Proof certificates have many useful applications, including the derivation of inductive validity cores [32], gaining
deeper insights on design behavior, deriving assume-guarantee verification conditions [37,53], deriving helper assertions during multi-property verification [36,29],
and generalizing to quantified domains (as elaborated later in §4.3).
When the property fails, AVR produces a counterexample trace that establishes how to reach a bad state (a state where the property is false) starting from
an initial state. AVR prints the counterexample witness in BTOR2 witness format [51], which allows for independent verification of the execution trace using
a BTOR2 witness simulator [4]. This allows the designer to debug and pin-point
the source of error by analyzing the execution leading to the buggy state.
3.3 Proof Race
AVR supports a variety of configurations and add-on features (as discussed
in §3.1). Without detailed knowledge of the input, it is hard to tell upfront which
technique will perform the best. Different configurations are useful to tackle different types of problems, though manually trying different configurations can
become tedious for the user. To counter this, AVR offers a multi-engine wrapper called proof race that automatically runs multiple instances of AVR with
different configurations in parallel and offers process-level parallelism. Given a
A. Goel and K. Sakallah
– Bounded model checking (BMC) [15] allows for an alternative to the IC3+SA
engine for quick bug hunting, especially for shallow bugs.
– Other options include adding global assumptions lazily, minimizing proof
certificates, making syntax-guided abstraction closer to (resp. farther from)
implicit predicate abstraction by decreasing (resp. increasing) abstraction
granularity, exploiting randomness during solving, and a few others.
Utilities
AVR also provides a number of useful utilities to the user including:
– Printing the problem in SMT-LIB format [13].
– Graphical visualizations of the problem and the word-level clause learning.
– Detailed statistics report on the input design and the verification run.
3.2 Certificates
Once a model checking problem is solved, there can be two possible outcomes:
either the property holds (safe), or it fails (unsafe).
If the property holds, IC3+SA produces an inductive invariant, i.e. an approximate fixpoint that establishes the property to be true in all executions of
the system. Inductive invariants act as proof certificates that guarantee the correctness of the verification outcome. AVR prints such proof certificates directly in
the SMT-LIB format, which allows for independent checking of their correctness
using an external SMT solver like Yices 2 or Z3. Since proof certificates are in
the word-level format, they are human-readable and much easier to relate to the
word-level input directly at the source-code level (as against bit-level invariants
which are usually too hard to understand). Proof certificates have many useful applications, including the derivation of inductive validity cores [32], gaining
deeper insights on design behavior, deriving assume-guarantee verification conditions [37,53], deriving helper assertions during multi-property verification [36,29],
and generalizing to quantified domains (as elaborated later in §4.3).
When the property fails, AVR produces a counterexample trace that establishes how to reach a bad state (a state where the property is false) starting from
an initial state. AVR prints the counterexample witness in BTOR2 witness format [51], which allows for independent verification of the execution trace using
a BTOR2 witness simulator [4]. This allows the designer to debug and pin-point
the source of error by analyzing the execution leading to the buggy state.
3.3 Proof Race
AVR supports a variety of configurations and add-on features (as discussed
in §3.1). Without detailed knowledge of the input, it is hard to tell upfront which
technique will perform the best. Different configurations are useful to tackle different types of problems, though manually trying different configurations can
become tedious for the user. To counter this, AVR offers a multi-engine wrapper called proof race that automatically runs multiple instances of AVR with
different configurations in parallel and offers process-level parallelism. Given a