---
_id: '4600'
abstract:
- lang: eng
  text: 'Model checking is a practical tool for automated debugging of embedded software.
    In model checking, a high-level description of a system is compared against a
    logical correctness requirement to discover inconsistencies. Since model checking
    is based on exhaustive state-space exploration and the size of the state space
    of a design grows exponentially with the size of the description, scalability
    remains a challenge. We have thus developed techniques for exploiting modular
    design structure during model checking, and the model checker jMocha (Java MOdel-CHecking
    Algorithm) is based on this theme. Instead of manipulating unstructured state-transition
    graphs, it supports the hierarchical modeling framework of reactive modules. jMocha
    is a growing interactive software environment for specification, simulation and
    verification, and is intended as a vehicle for the development of new verification
    algorithms and approaches. It is written in Java and uses native C-code BDD libraries
    from VIS. jMocha offers: (1) a GUI that looks familiar to Windows/Java users;
    (2) a simulator that displays traces in a message sequence chart fashion; (3)
    requirements verification both by symbolic and enumerative model checking; (4)
    implementation verification by checking trace containment; (5) a proof manager
    that aids compositional and assume-guarantee reasoning; and (6) SLANG (Scripting
    LANGuage) for the rapid and structured development of new verification algorithms.
    jMocha is available publicly at ; it is a successor and extension of the original
    Mocha tool that was entirely written in C.'
acknowledgement: 'We thank Himyanshu Anand, Ben Horowitz, Franjo Ivancic, Michael
  McDougall, Marius Minea, Oliver Moeller. Shaz Qadeer, Sriram Rajamani, and Jean-Francois
  Raskin for their assistance in the development of JMOCHA. The MOCHA project is funded
  in part by the DARPA grant NAG2-1214, the NSF CAREER awards CCR95-01708 and CCR97-34115,
  the NSF grant CCR99-70925, the NSF ITR grant CCR0085949, the MARC0 grant 98-DT-660,
  and the SRC contracts 99-TJ-683.003 and 99-TJ-688. '
article_processing_charge: No
author:
- first_name: Rajeev
  full_name: Alur, Rajeev
  last_name: Alur
- first_name: Luca
  full_name: De Alfaro, Luca
  last_name: De Alfaro
- first_name: Radu
  full_name: Grosu, Radu
  last_name: Grosu
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Myong
  full_name: Kang, Myong
  last_name: Kang
- first_name: Christoph
  full_name: Kirsch, Christoph
  last_name: Kirsch
- first_name: Ritankar
  full_name: Majumdar, Ritankar
  last_name: Majumdar
- first_name: Freddy
  full_name: Mang, Freddy
  last_name: Mang
- first_name: Bow
  full_name: Wang, Bow
  last_name: Wang
citation:
  ama: 'Alur R, De Alfaro L, Grosu R, et al. jMocha: A model-checking tool that exploits
    design structure. In: <i>Proceedings of the 23rd International Conference on Software
    Engineering</i>. IEEE; 2001:835-836. doi:<a href="https://doi.org/10.1109/ICSE.2001.919196">10.1109/ICSE.2001.919196</a>'
  apa: 'Alur, R., De Alfaro, L., Grosu, R., Henzinger, T. A., Kang, M., Kirsch, C.,
    … Wang, B. (2001). jMocha: A model-checking tool that exploits design structure.
    In <i>Proceedings of the 23rd International Conference on Software Engineering</i>
    (pp. 835–836). IEEE. <a href="https://doi.org/10.1109/ICSE.2001.919196">https://doi.org/10.1109/ICSE.2001.919196</a>'
  chicago: 'Alur, Rajeev, Luca De Alfaro, Radu Grosu, Thomas A Henzinger, Myong Kang,
    Christoph Kirsch, Ritankar Majumdar, Freddy Mang, and Bow Wang. “JMocha: A Model-Checking
    Tool That Exploits Design Structure.” In <i>Proceedings of the 23rd International
    Conference on Software Engineering</i>, 835–36. IEEE, 2001. <a href="https://doi.org/10.1109/ICSE.2001.919196">https://doi.org/10.1109/ICSE.2001.919196</a>.'
  ieee: 'R. Alur <i>et al.</i>, “jMocha: A model-checking tool that exploits design
    structure,” in <i>Proceedings of the 23rd International Conference on Software
    Engineering</i>, 2001, pp. 835–836.'
  ista: 'Alur R, De Alfaro L, Grosu R, Henzinger TA, Kang M, Kirsch C, Majumdar R,
    Mang F, Wang B. 2001. jMocha: A model-checking tool that exploits design structure.
    Proceedings of the 23rd International Conference on Software Engineering. ICSE:
    Software Engineering, 835–836.'
  mla: 'Alur, Rajeev, et al. “JMocha: A Model-Checking Tool That Exploits Design Structure.”
    <i>Proceedings of the 23rd International Conference on Software Engineering</i>,
    IEEE, 2001, pp. 835–36, doi:<a href="https://doi.org/10.1109/ICSE.2001.919196">10.1109/ICSE.2001.919196</a>.'
  short: R. Alur, L. De Alfaro, R. Grosu, T.A. Henzinger, M. Kang, C. Kirsch, R. Majumdar,
    F. Mang, B. Wang, in:, Proceedings of the 23rd International Conference on Software
    Engineering, IEEE, 2001, pp. 835–836.
conference:
  name: 'ICSE: Software Engineering'
date_created: 2018-12-11T12:09:41Z
date_published: 2001-08-07T00:00:00Z
date_updated: 2023-05-08T14:06:55Z
day: '07'
doi: 10.1109/ICSE.2001.919196
extern: '1'
language:
- iso: eng
month: '08'
oa_version: None
page: 835 - 836
publication: Proceedings of the 23rd International Conference on Software Engineering
publication_identifier:
  isbn:
  - '0769510507'
publication_status: published
publisher: IEEE
publist_id: '109'
quality_controlled: '1'
status: public
title: 'jMocha: A model-checking tool that exploits design structure'
type: conference
user_id: ea97e931-d5af-11eb-85d4-e6957dddbf17
year: '2001'
...