Overview

McScM (Model Checker for Systems of Communicating fifo Machines) is a small framework for implementing model checking algorithms in the context of infinite state systems of the form "finite control plus infinite data". The main constituent is the verify tool for the safety verification of distributed machines that communicate asynchronously via reliable fifo channels. The framework is implemented in Objective Caml and published under a BSD license.