User Tools

Site Tools


Mace Modelchecker Documentation

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].

FAQ Pages

Errata (Bugs)

Property Parsing


  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.
macemc.txt · Last modified: 2012/10/13 02:15 by mwalraed