MCMT: Experiments

Timings have been obtained on a Pentium Intel 1.73 GHz with 1 Gb Sdram running MCMT v.1.0 on Gentoo Linux. Further documentation on single examples is available in the distribution. In the first table, statistics are relative to the default configuration of the tool, whereas the second table refers to the best setting we found for each example (thus, in the second table, various heuristics for invariant synthesis, signature abstraction and acceleration can have been applied). We are far from having explored all possible settings, we just tried few of them, hence the real 'best setting' has sometimes still to be found.
Timeouts are mostly due to trivial divergence reasons that the default setting is not able to capture. A couple of lines of the Default Setting Table are empty: this is because a non-default setting has been adopted in order to manually suggest the tool invariants to be checked (these are the only two cases where invariants are not generated automatically).