Abstract

The Mono Model Checker (MMC) is a software model checker that can verify whether a .NET program contains assertion violations or deadlocks. It was developed as part of a Master's project by Niels Aan de Brugh. Much of its design was inspired by Java PathFinder, a software model checker for Java programs. This thesis is the result of the follow-up Master's project on MMC. The goal during this project was to improve MMC's ability to verify models with larger state spaces.

Enhancements have been added in all areas. For improving MMC's performance, both partial order reduction (POR) using object escape analysis and stateful dynamic POR have been added. These techniques reduce the size of a model's state space, and hence reduce the time and memory needed for its verification. For improving MMC's usefulness, .NET's exception handling has been fully implemented, more instructions have been added for increased .NET compliance and a comprehensive testing framework has been created. The latter employs Microsoft's own .NET virtual machine testing suite and has revealed numerous bugs. For improving MMC's usability, an error tracer has been added. It shows the sequence of instructions leading to the assertion violation or deadlock. This improves the user's understanding of detected errors.

Besides improving MMC with known techniques, during the course of this Master's project, three new techniques were developed that effectively decrease both time and memory needed for verifying a model. To decrease memory use, a collapsing scheme has been developed for collapsing the meta-data used by a stateful dynamic POR. The reduction of memory is more than a factor of two. To decrease the verification time, a Memoised Garbage Collector has been developed. It has a lower time-complexity than the often used Mark & Sweep garbage collector. Its main idea is that it only traverses changed parts of the heap instead of the full heap. The average time reduction is between 9% and 26%, depending on the model that is verified. The third technique is called incremental hashing, which also has a lower time-complexity. The key notion in this hashing scheme is that a hashcode of an array is recalculated using the old hashcode and the changes to the array. Though this technique was originally developed for MMC, we implemented in Spin, because the stake of hashing in MMC is near zero.

Experiments with the BEEM benchmarks showed up to 20% reduction in time when compared against Jenkins' hash function, which is an often used hash function in model checking due to its good uniformity.

We also benchmarked MMC against JPF and Bandera using the Java Grande Benchmark models. The results indicate that MMC is faster in terms of states per second, but JPF is more effective in reducing the state space. Bandera is on all fronts no match for MMC and JPF, as it is outperformed in every benchmark.

Additional Resources

1. The paper