MOCHA: Modularity in Model Checking. 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).
Keywords for this software
References in zbMATH (referenced in 92 articles )
Showing results 81 to 92 of 92.
- Finkbeiner, Bernd: Language containment checking with nondeterministic BDDs (2001)
- Kremer, Steve; Raskin, Jean-François: A game-based verification of non-repudiation and fair exchange protocols (2001)
- Levi, Francesca: Compositional verification of quantitative properties of statecharts (2001)
- Möller, M. Oliver; Alur, Rajeev: Heuristics for hierarchical partitioning with application to model checking (2001)
- Alur, Rajeev; Grosu, Radu: Modular refinement of hierarchic reactive machines (2000)
- Alur, R.; Grosu, R.; McDougall, M.: Efficient reachability analysis of hierarchical reactive machines (2000)
- Ball, Thomas; Rajamani, Sriram K.: Bebop: A symbolic model checker for Boolean programs (2000)
- Foster, Jeffrey S.; Fähndrich, Manuel; Aiken, Alexander: Polymorphic versus monomorphic flow-insensitive points-to analysis for C (2000)
- Henzinger, Thomas A.: Exploiting design structure in model checking. (Abstract) (2000)
- McMillan, K. L.: A methodology for hardware verification using compositional model checking (2000)
- Henzinger, Thomas A.; Qadeer, Shaz; Rajamani, Sriram K.: Assume-guarantee refinement between different time scales (1999)
- Henzinger, Thomas A.; Qadeer, Shaz; Rajamani, Sriram K.: Verifying sequential consistency on shared-memory multiprocessor systems (1999)