Ecole Polytechnique Fédérale de Lausanne
Mocha Project
english only

Mocha: Exploiting Modularity in Model Checking

MOCHA is a joint project between the University of California at Berkeley, the University of Pennsylvania, and the State University of New York at Stony Brook; and is funded in part by the Defense Advanced Research Projects Agency (DARPA (NASA) grant NAG2-1214), the National Science Foundation (NSF CAREER award CCR95-01708 and CCR97-34115, and award CCR99-70925), the Microelectronics Advanced Research Corporation (MARCO grant 98-DT-660), and the Semiconductor Research Corporation (SRC contract 99-TJ-683.003 and 99-TJ-688).

MOCHA is a growing interactive software environment for system specification and verification. The main objective of MOCHA is to exploit, rather than destroy, design structure in automatic verification. MOCHA is intended as a vehicle for development of new verification algorithms and approaches. MOCHA is available in two versions, cMocha (Version 1.0.1) and jMocha (Version 2.0).

Both versions offer the following capabilities:

The Mocha Team

The Mocha Demo

The Mocha Papers and References

The Mocha Files