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.