@inproceedings{4600,
  abstract     = {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.},
  author       = {Alur, Rajeev and De Alfaro, Luca and Grosu, Radu and Henzinger, Thomas A and Kang, Myong and Kirsch, Christoph and Majumdar, Ritankar and Mang, Freddy and Wang, Bow},
  booktitle    = {Proceedings of the 23rd International Conference on Software Engineering},
  isbn         = {0769510507},
  pages        = {835 -- 836},
  publisher    = {IEEE},
  title        = {{jMocha: A model-checking tool that exploits design structure}},
  doi          = {10.1109/ICSE.2001.919196},
  year         = {2001},
}