Mocha Home Page
University of California at Berkeley
Department of Electrical Engineering and Computer Sciences
University of Pennsylvania
Department of Computer and Information Science
State University of New York at Stony Brook
Department of Computer Science

Technical References for Mocha

  • The MOCHA system was announced at CAV 1998:

    Rajeev Alur, Thomas A. Henzinger, F.Y.C. Mang, Shaz Qadeer, Sriram K. Rajamani, and Serdar Tasiran. Mocha: Modularity in model checking. In Proceedings of the Tenth International Conference on Computer-aided Verification (CAV 1998), Lecture Notes in Computer Science 1427, Springer-Verlag, 1998, pp. 521-525. Abstract.
  • There is a tool paper on the new Java implementation of MOCHA:

    L. de Alfaro, R. Alur, R. Grosu, T. Henzinger, M. Kang, R. Majumdar, F. Mang, C. Meyer-Kirsch, and B.Y. Wang. Mocha: Exploiting Modularity in Model Checking. Full paper.
  • MOCHA employs the modeling framework of reactive modules:

    Rajeev Alur and Thomas A. Henzinger. Reactive modules. Formal Methods in System Design 15:7-48, 1999. A preliminary version appeared in the Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science (LICS 1996), pp. 207-218. Abstract.

    Rajeev Alur and Thomas A. Henzinger. Reactive Modules. Chapter 1 in Computer-Aided Verification: An introduction to model building and model checking for concurrent systems.
  • The specification language of MOCHA is alternating-time temporal logic:

    Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time temporal logic. In Proceedings of the 38th Annual IEEE Symposium on Foundations of Computer Science (FOCS 1997), pp. 100-109. Abstract.
  • MOCHA provides support for a range of compositional and hierarchical verification methodologies. Assume-guarantee rules provided by MOCHA are described in:

    Rajeev Alur, Radu Grosu, and Bow-Yaw Wang. Automated refinement checking for asynchronous processes. In Proceedings of the Third International Conference on Formal Methods in Computer-Aided Design (FMCAD'00). Abstract, Full Paper.

    Thomas A. Henzinger, Xiaojun Liu, Shaz Qadeer, and Sriram K. Rajamani. Formal specification and verification of a dataflow processor array. In Proceedings of the IEEE/ACM International Conference on Computer-aided Design (ICCAD 1999), pp. Abstract.

    Rajeev Alur, Luca de Alfaro, Thomas A. Henzinger, and F.Y.C. Mang. Automating modular verification. In Proceedings of the Tenth International Conference on Concurrency Theory (CONCUR 1999), Lecture Notes in Computer Science 1664, Springer-Verlag, 1999, pp. 82-97. Abstract.

    Thomas A. Henzinger, Shaz Qadeer, and Sriram K. Rajamani. Verifying sequential consistency for multiprocessor memory protocols. In Proceedings of the 11th International Conference on Computer-aided Verification (CAV 1999), Lecture Notes in Computer Science 1633, Springer-Verlag, 1999, pp. 301-315. Abstract.

    Thomas A. Henzinger, Shaz Qadeer, and Sriram K. Rajamani. Assume-guarantee refinement between different time scales. In Proceedings of the 11th International Conference on Computer-aided Verification (CAV 1999), Lecture Notes in Computer Science 1633, Springer-Verlag, 1999, pp. 208-221. Abstract.

    Thomas A. Henzinger, Shaz Qadeer, and Sriram K. Rajamani. You assume, we guarantee: methodology and case studies. In Proceedings of the Tenth International Conference on Computer-aided Verification (CAV 1998), Lecture Notes in Computer Science 1427, Springer-Verlag, 1998, pp. 440-451. Abstract.
  • On-the-fly model checking based on hierarchical reduction algorithms in MOCHA are described in:

    Rajeev Alur and Bow-Yaw Wang. ``Next'' heuristic for on-the-fly model checking. In Proceedings of the Tenth International Conference on Concurrency Theory (CONCUR 1999), Lecture Notes in Computer Science 1664, Springer Verlag, 1999. Abstract. Full paper.
  • Other interesting and related papers can be found here as well as here and here .

Please send questions or comments about MOCHA here.
This site is maintained by the mocha-webmaster.
Mirror sites are maintained at the University of California at Berkeley and the University of Pennsylvania.
Last modified: Thursday, 08-Aug-00 16:44:58,  1465 Hits