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).

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"