MoonWalker

MoonWalker is a software model checker for CIL bytecode, the bytecode of .NET programs. MoonWalker is able to detect deadlocks and assertion violations in CIL programs. MoonWalker has been developed on the Mono platform. The design of MoonWalker is inspired by and based on the Java PathFinder (JPF), a model checker for Java programs.

MoonWalker was previously known as MMC, the Mono Model Checker. Due to several name clashes, however, the name of the software model checker has been changed to MoonWalker.

MoonWalker has been developed in the Formal Methods and Tools (FMT) group of the University of Twente.
Contact person for MoonWalker: Theo Ruys.

Files

This binary distribution of MoonWalker 1.0.1 contains the following files:

README.html: this file
LICENSE.txt: Apache 2.0 license
bin/moonwalker.exe: MoonWalker executable
bin/Mono.Cecil.dll: Mono's Cecil library (version 0.6), needed by MoonWalker.
bin/C5*: C5 library (version 1.0.2), needed by MoonWalker.
examples/*.cs: some C# examples

MoonWalker 1.0.1 has been compiled with Mono 1.2.6 under Mac OS X 10.4.11.

Installation

MoonWalker has been developed under Mono and Windows XP/Vista.
Being a CIL assembly, MoonWalker should work on Windows XP/Vista and on all Mono platforms.
The bin directory of the binary distribution contains all files needed to run MoonWalker. The moonwalker.exe file can be installed anywhere, as long as both *.dll files are placed in the same directory.

Running MoonWalker

First, compile a C# source program to CIL bytecode, e.g. using Mono's C# compiler:

    mcs Deadlock.cs

If the C# program contains assertion checks, compile the model with -d:DEBUG, otherwise the assertion checks are not compiled into the resulting assembly.
Next, run MoonWalker on the generated CIL bytecode:

    mono moonwalker.exe -a Deadlock.exe

If MoonWalker finds an error in the program (i.e. a deadlock or assertion violation) it will write a trace leading to the error into a file with extension .trace (in the above example this would be Deadlock.exe.trace). A useful extra option to MoonWalker is -s which shows statistics on the verification run.
To get a list of all supported options:

    mono moonwalker.exe -h

Licenses

MoonWalker itself is released under the Apache 2.0 license.
Cecil is a Mono class library which is released under the MIT X11 license.
C5 is released under a MIT-style open license.

Version history

1.0.1	2008.04.11	First public release of MoonWalker (binary and source).
1.0.0	2007.12.19	New version after MSc Project by Viet Yen Nguyen. Much improved performance due to optimisations like, e.g. , dynamic partial order reduction, memoised garbage collection, structured exception handling mechanism.
0.5.5	2007.03.28	Bytecode 2007 version: improved error trace + state information.
0.5.1	2006.12.18	First public release (binary only).
0.5	2006.08.28	Initial version after MSc Project of Niels Aan de Brugh.

This page has last been updated by Theo Ruys on Friday, 11 April 2008.