Introduction

MoonWalker is a model checker developed on the Mono platform. MoonWalker is a program to automatically detect errors in CIL bytecode programs, i.e. applications written for the .NET platform.

The current version of MoonWalker is able to find deadlocks and assertion violations in CIL programs, generated with Mono's C# compiler.

The design of MoonWalker is inspired by and based on the Java PathFinder, a model checker for Java programs.

MoonWalker has been developed in the Formal Methods and Tools group of the University of Twente. For further information on MoonWalker, please contact Theo Ruys.

Moon is an anagram of Mono. Walker refers to the nature of the tool: walking the state space of CIL bytecode 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.

Download

The current version of MoonWalker is 1.0.1.
The binary distribution can be downloaded here: moonwalker-1.0.1.zip.
The README.html within this distribution explains how MoonWalker should be installed and used.
There is also a MoonWalker project at Google Code, where the source code of MoonWalker can be retrieved. Notes:

  • MoonWalker requires Mono's the Cecil library and the C5 library to run.
    Both libraries are included in the binary distribution.
  • MoonWalker has been compiled with Mono version 1.2.6.
  • MoonWalker has only been tested on Mac OS X 10.4.x with Mono, and Windows XP/Vista.
    (From several Linux users we have heard, however, that it runs smoothly on Linux using Mono as well.)

Documentation

  • Niels H.M. Aan de Brugh, Viet Yen Nguyen, and Theo C. Ruys.
    MoonWalker: verification of .NET programs.
    Proceedings of TACAS 2009, York, UK, March 22-29, 2009, pp. 170-173.
    This paper gives a short, technical overview of the new features of MoonWalker 1.0.

  • Viet Yen Nguyen and Theo C. Ruys.
    Memoised Garbage Collection for Software Model Checking.
    Proceedings of TACAS 2009, York, UK, March 22-29, 2009, pp. 201-214.
    This paper describes the memoised garbage collection algorithm as implemented in MoonWalker 1.0.

  • Theo C. Ruys and Niels H.M. Aan de Brugh.
    MMC: the Mono Model Checker.
    Proceedings of 2nd Workshop on Bytecode 2007, Braga, Portugal, April 2007.
    ENTCS 190 (1), 2007, pp. 149-160.
    This paper gives an introduction and overview of MoonWalker 0.5.

  • Viet Yen Nguyen.
    Optimising Techniques for Model Checkers.
    MSc Thesis, University of Twente, The Netherlands, December 2007.
    This MSc thesis describes the design and implementation of the new features of MoonWalker 1.0 in detail.

  • Niels Aan de Brugh.
    Software Model Checking for Mono.
    MSc Thesis, University of Twente, The Netherlands, August 2006.
    This MSc thesis describes the design and implementation of MoonWalker 0.5 in detail.

People

  • Niels Aan de Brugh: principal designer of MoonWalker 0.5.
  • Viet Yen Nguyen: principal designer of MoonWalker 1.0.
  • Theo Ruys: supervisor of MoonWalker project.

Version history

version date features
1.0.1 11 Apr 2008 First official MoonWalker release:
  • name of the tool has been changed to MoonWalker
  • first source code release via Google Code
1.0.0 19 Dec 2007 New features:
  • partial order reduction using object escape analysis
  • stateful dynamic partial order reduction
  • collapsion of summarised interleaving information for dynamic POR
  • memoised garbage collection
  • structured exception handling mechanism
  • error tracer
  • extensive testing framework
0.5.5 28 Mar 2007 Bytecode 2007 version. Added features:
  • refactored with generics
  • improved error trace + state information
  • ported to .NET 2.0
0.5.1 18 Dec 2006 First public binary release.
0.5 28 Aug 2006 Initial version. Features:
  • verification of deadlocks and assertion violations
  • structured state collapse compression
  • backtracking using delta's
  • heap canonicalisation using symmetry reductions
  • mark & sweep garbage collection