MOCHA

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

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 92 articles )

Showing results 61 to 80 of 92.
Sorted by year (citations)
  1. Wooldridge, Michael; van der Hoek, Wiebe: On obligations and normative ability: Towards a logical analysis of the social contract (2005)
  2. Xie, Gaoyan; Dang, Zhe: An automata-theoretic approach for model-checking systems with unspecified components (2005)
  3. Abramsky, Samson; Ghica, Dan R.; Murawski, Andrzej S.; Ong, C.-H. Luke: Applying game semantics to compositional software modeling and verification (2004)
  4. Contensin, Magali; Pierre, Laurence: Model-checking systems with unbounded variables without abstraction (2004)
  5. de la Riva, Claudio; Tuya, Javier: Modular model checking of software specifications with simultaneous environment generation (2004)
  6. Ioustinova, Natalia; Sidorova, Natalia; Steffen, Martin: Synchronous closing and flow analysis for model checking timed systems (2004)
  7. Kacprzak, M.; Penczek, W.: A SAT-based approach to unbounded model checking for alternating-time temporal epistemic logic (2004)
  8. Sirjani, Marjan; Movaghar, Ali; Shali, Amin; de Boer, Frank S.: Modeling and verification of reactive systems using Rebeca (2004)
  9. Win, Toh Ne; Ernst, Michael D.; Garland, Stephen J.; Kırlı, Dilsun; Lynch, Nancy A.: Using simulated execution in verifying distributed algorithms (2004) ioport
  10. López, Javier; Ortega, Juan J.; Troya, José M.: Applying SDL to formal analysis of security systems (2003)
  11. Madhusudan, P.; Nam, Wonhong; Alur, Rajeev: Symbolic computational techniques for solving games (2003)
  12. Win, Toh Ne; Ernst, Michael D.; Garland, Stephen J.; Kirli, Dilsun; Lynch, Nancy A.: Using simulated execution in verifying distributed algorithms (2003)
  13. Chaki, Sagar; Rajamani, Sriram K.; Rehof, Jakob: Types as models: model checking message-passing programs (2002)
  14. Harding, Aidan; Ryan, Mark; Schobbens, Pierre-Yves: Approximating ATL(^*) in ATL (2002)
  15. Ioustinova, Natalia; Sidorova, Natalia; Steffen, Martin: Closing open SDL-systems for model checking with DTSpin (2002)
  16. Santone, Antonella: Automatic verification of concurrent systems using a formula-based compositional approach (2002)
  17. Sidorova, Natalia; Steffen, Martin: Synchronous closing of timed SDL systems for model checking (2002)
  18. Wand, Mitchell; Williamson, Galen B.: A modular, extensible proof method for small-step flow analyses (2002)
  19. Cassez, Franck; Ryan, Mark Dermot; Schobbens, Pierre-Yves: Proving feature non-interaction with alternating-time temporal logic (2001)
  20. Doche, M.; Vernier-Mounier, I.; Kordon, F.: A modular approach to the specification and validation of an electrical flight control system (2001)