“The only reasonable way to get a program right is to assume that it will at first contain errors and take steps to discover these and correct them.”
|--(Christopher Strachey, 1916–1975)|
This chapter summarizes all verification options. The options apply to the verification code that is generated with SPIN’s run-time option
-a. Also included is an explanation of the information that is generated by the program at the end of a verification run (unless disabled with PAN run-time option
The three main sections of this chapter cover:
PAN Compile-Time Options:
Options that are available at the time of compilation of the verifier source code.
PAN Run-Time Options:
Options that are available as command-line arguments ...