Chapter 4
Program Termination

The program terminates if the safety properties can be proved, or if the number of abstract states exceeds a certain bound, or if the maximal box diameter after calling the splitting and pruning algorithm is less than the given float.

Note that the default value for the maximal number of abstract states is 1000 and the default value for the maximal box diameter bound is 0.01. The user can run “./hsolver -h” for help and then choose other values.