Verification preference page

The most complex preference page in SpinRCP is the Verification preference page. In the upper part the user can export current verification parameters (verification profile) to an xml file and import or reload a previously saved verification profile. Verification options are accessible below in two tabs: Basic Options and Advanced Options.

In the Basic Options tab a user can select a correctness property to be proved (either safety or liveness) with several additional options, the search mode (exhaustive, bitstate hashing or hash-compact), how a full queue behaves in verification (either blocks or loses new messages), the explicit use of user entered compile-time and run-time parameters that supersede the clicked options and elsewhere entered parameters, and how a never claim (if any) is specified. A never claim can be specified in four different ways. In the Advanced Options tab it is possible to enter several advanced verification parameters (the amount of the available physical memory in megabytes, the estimated state space size, the maximum search depth, number of hash-functions in bitstate mode, extra verifier generation options, extra compile-time directives, and extra run-time options) and select some error-trapping and verification run type options.