Welcome to the documentation for the modelchecker. The Mace modelchecker automatically checks your distributed systems code written in Mace, against user level expectations. This work has been published in [1].

• Getting started with the Modelchecker
• Understanding the modelchecker's output
• Debugging with the Modelchecker
• Sample out-of-mace project with Modelchecker

• Properties
• Using MaceMC, error messages, etc.

• Mace Property Parser Cannot Parse *x

1. Life, Death, and the Critical Transition: Detecting Liveness Bugs in Systems Code. Charles Killian, James W. Anderson, Ranjit Jhala, and Amin Vahdat, in Proceedings of NSDI (NSDI 2007), Cambridge, MA, April 2007. PDF Awarded Best Paper.