Abstract

Software has become larger and more complex than the human mind can grasp. This results in software that can contain errors, even when the software is thoroughly tested. Automated validation techniques can be a helping hand in the process of eliminating these errors. Specifically, model checking techniques can be used to systematically "test" all possible executions of the software, finding possible errors automatically.

The development of tools to facilitate this can be considered a new trend in research on validation techniques. Parallel to this trend, a software development platform called .NET was released by Microsoft. This platform runs applications written in many different programming languages. Mono is a free and open implementation of .NET. This MSc project is an attempt to combine both the error-hunting capabilities of software model checking and the versatility of the Mono platform.

In the course of more than a year we have written our own model checking virtual machine, capable of checking applications in one of the many languages that can be compiled to run on .NET and Mono. In many respects the approach is similar to the Java PathFinder, a tool to model check Java applications, developed at Nasa. We introduce the reader to the background of Mono and software model checking. Then we discuss our implementation in full detail, explaining design choices and algorithms used. Finally, we present some experimental data, suggest several improvements that may be useful to investigate in the future.

Additional Resources

1. The paper