Settings

In doubt, you should always use the default setting. Other settings are often not tested very well and many combinations of settings are incompatible to each other.

Specification-related settings

Checked kinds of specifications

If the input is a Boogie program, we check all kinds of specifications (assert, requires, ensures, invariant). If the input is a C program, we check the specifications that are enabled in the CACSL2BoogieTranslator plug-in.

Detailedness of result list.

There are two modes. In one the verification is stopped after the first violation was found. In the other mode all specifications are analyzed sequentially and for each a result is returned.

Tool Plugins > Automizer > "Stop after first violation was found" Please note that this has major implications with the "Assume correctness of other specifications" setting.

Assume correctness of other specifications.

There are two modes. In one the analysis of a specification is independent of all other specifications. In the other mode we analyse each specification under the assumption that all other specifications are correct.

The difference can be explained on the following example.

int x := getSomeRandomValue();
assert x == 5;
assert x >= 0;

In the first mode, we report that both assert statements can be violated. In the second mode, we report only that the first assert statement can be violated (because under the assumption that x == 5 holds, the inequality x >= 0 also holds).

The corresponding setting is Tool Plugins > RCFGBuilder > "Add additional assume for each assert." (If set to false, the first mode is used. If set to true the second mode is used.)

Performance-related settings.

Block Encoding

Larger Blocks: smaller automata, but larger formula. Smaller Blocks: smaller formula, but larger automata.

Tool Plugins > RCFGBuiler > "Size of a code block"

Interpolant automaton enhancement

We check Hoare triples. Depending on the result, we may add additional edges.

1. PREDICATE_ABSTRACTION (default) Use as predicates the interpolants (of a trace check) and conjunctions of interpolants.

2. PREDICATE_ABSTRACTION_CONSERVATIVE (most precise, most expensive) Use as predicates all conjuncts of all interpolants. Additionally, use also all conjunctions of all conjuncts.

3. EAGER Use as predicates all interpolants and conjunctions of interpolants. A check of the Hoare triple { Φ_1 /\ ... /\ Φ_n } st { Ψ_1 /\ ... /\ Ψ_m } is approximated by checking instead { Φ_i } st { Ψ_j } for all 1<=i<=n, 1<=j<=m.

4. EAGER_CONSERVATIVE Similar to EAGER, but we check { Φ_i } st { Ψ_j } only if Ψ_j==Φ_i or Ψ_j==false