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).


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)