-
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).
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.
|
This site is maintained by the mocha-webmaster. Mirror sites are maintained at the University of California at Berkeley and the SUNY at Stony Brook. |
|
|