[{"citation":{"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.","mla":"Alur, Rajeev, et al. “JMocha: A Model-Checking Tool That Exploits Design Structure.” Proceedings of the 23rd International Conference on Software Engineering, IEEE, 2001, pp. 835–36, doi:10.1109/ICSE.2001.919196.","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 Proceedings of the 23rd International Conference on Software Engineering, 835–36. IEEE, 2001. https://doi.org/10.1109/ICSE.2001.919196.","ama":"Alur R, De Alfaro L, Grosu R, et al. jMocha: A model-checking tool that exploits design structure. In: Proceedings of the 23rd International Conference on Software Engineering. IEEE; 2001:835-836. doi:10.1109/ICSE.2001.919196","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 Proceedings of the 23rd International Conference on Software Engineering (pp. 835–836). IEEE. https://doi.org/10.1109/ICSE.2001.919196","ieee":"R. Alur et al., “jMocha: A model-checking tool that exploits design structure,” in Proceedings of the 23rd International Conference on Software Engineering, 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."},"publication":"Proceedings of the 23rd International Conference on Software Engineering","page":"835 - 836","quality_controlled":"1","doi":"10.1109/ICSE.2001.919196","date_published":"2001-08-07T00:00:00Z","conference":{"name":"ICSE: Software Engineering"},"language":[{"iso":"eng"}],"article_processing_charge":"No","publication_identifier":{"isbn":["0769510507"]},"day":"07","month":"08","_id":"4600","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. ","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","year":"2001","publisher":"IEEE","title":"jMocha: A model-checking tool that exploits design structure","publication_status":"published","status":"public","author":[{"first_name":"Rajeev","last_name":"Alur","full_name":"Alur, Rajeev"},{"last_name":"De Alfaro","first_name":"Luca","full_name":"De Alfaro, Luca"},{"last_name":"Grosu","first_name":"Radu","full_name":"Grosu, Radu"},{"full_name":"Henzinger, Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","last_name":"Henzinger","first_name":"Thomas A"},{"first_name":"Myong","last_name":"Kang","full_name":"Kang, Myong"},{"full_name":"Kirsch, Christoph","first_name":"Christoph","last_name":"Kirsch"},{"first_name":"Ritankar","last_name":"Majumdar","full_name":"Majumdar, Ritankar"},{"last_name":"Mang","first_name":"Freddy","full_name":"Mang, Freddy"},{"last_name":"Wang","first_name":"Bow","full_name":"Wang, Bow"}],"oa_version":"None","date_updated":"2023-05-08T14:06:55Z","date_created":"2018-12-11T12:09:41Z","type":"conference","publist_id":"109","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."}],"extern":"1"},{"month":"03","publication_identifier":{"issn":["0925-9856"]},"doi":"10.1023/A:1008767206905","language":[{"iso":"eng"}],"quality_controlled":"1","publist_id":"108","extern":"1","author":[{"full_name":"Alur, Rajeev","first_name":"Rajeev","last_name":"Alur"},{"full_name":"Brayton, Robert","last_name":"Brayton","first_name":"Robert"},{"full_name":"Henzinger, Thomas A","first_name":"Thomas A","last_name":"Henzinger","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724"},{"full_name":"Qadeer, Shaz","last_name":"Qadeer","first_name":"Shaz"},{"full_name":"Rajamani, Sriram","first_name":"Sriram","last_name":"Rajamani"}],"date_updated":"2023-05-08T12:22:38Z","date_created":"2018-12-11T12:09:41Z","volume":18,"acknowledgement":"Gerard Holzmann provided us with information on SPIN. Ken McMillan and Doron Peled contributed through discussions. The VIS group at UC Berkeley and Rajeev Ranjan in particular helped with the experiments.","year":"2001","publication_status":"published","publisher":"Springer","day":"01","article_processing_charge":"No","scopus_import":"1","date_published":"2001-03-01T00:00:00Z","publication":"Formal Methods in System Design","citation":{"apa":"Alur, R., Brayton, R., Henzinger, T. A., Qadeer, S., & Rajamani, S. (2001). Partial-order reduction in symbolic state-space exploration. Formal Methods in System Design. Springer. https://doi.org/10.1023/A:1008767206905","ieee":"R. Alur, R. Brayton, T. A. Henzinger, S. Qadeer, and S. Rajamani, “Partial-order reduction in symbolic state-space exploration,” Formal Methods in System Design, vol. 18, no. 2. Springer, pp. 97–116, 2001.","ista":"Alur R, Brayton R, Henzinger TA, Qadeer S, Rajamani S. 2001. Partial-order reduction in symbolic state-space exploration. Formal Methods in System Design. 18(2), 97–116.","ama":"Alur R, Brayton R, Henzinger TA, Qadeer S, Rajamani S. Partial-order reduction in symbolic state-space exploration. Formal Methods in System Design. 2001;18(2):97-116. doi:10.1023/A:1008767206905","chicago":"Alur, Rajeev, Robert Brayton, Thomas A Henzinger, Shaz Qadeer, and Sriram Rajamani. “Partial-Order Reduction in Symbolic State-Space Exploration.” Formal Methods in System Design. Springer, 2001. https://doi.org/10.1023/A:1008767206905.","short":"R. Alur, R. Brayton, T.A. Henzinger, S. Qadeer, S. Rajamani, Formal Methods in System Design 18 (2001) 97–116.","mla":"Alur, Rajeev, et al. “Partial-Order Reduction in Symbolic State-Space Exploration.” Formal Methods in System Design, vol. 18, no. 2, Springer, 2001, pp. 97–116, doi:10.1023/A:1008767206905."},"article_type":"original","page":"97 - 116","abstract":[{"lang":"eng","text":"State-space explosion is a fundamental obstacle in the formal verification of designs and protocols. Several techniques for combating this problem have emerged in the past few years, among which two are significant: partial-order reduction and symbolic state-space search. In asynchronous systems, interleavings of independent concurrent events are equivalent, and only a representative interleaving needs to be explored to verify local properties. Partial-order methods exploit this redundancy and visit only a subset of the reachable states. Symbolic techniques, on the other hand, capture the transition relation of a system and the set of reachable states as boolean functions. In many cases, these functions can be represented compactly using binary decision diagrams (BDDs). Traditionally, the two techniques have been practiced by two different schools—partial-order methods with enumerative depth-first search for the analysis of asynchronous network protocols, and symbolic breadth-first search for the analysis of synchronous hardware designs. We combine both approaches and develop a method for using partial-order reduction techniques in symbolic BDD-based invariant checking. We present theoretical results to prove the correctness of the method, and experimental results to demonstrate its efficacy."}],"issue":"2","type":"journal_article","oa_version":"None","_id":"4599","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","status":"public","title":"Partial-order reduction in symbolic state-space exploration","intvolume":" 18"},{"language":[{"iso":"eng"}],"date_published":"2001-06-01T00:00:00Z","doi":"10.1145/503209.503226","conference":{"end_date":"2001-09-14","start_date":"2001-09-10","location":"Vienna, Austria","name":"FSE: Foundations of Software Engineering"},"page":"109 - 120","quality_controlled":"1","citation":{"mla":"De Alfaro, Luca, and Thomas A. Henzinger. “Interface Automata.” Proceedings of the 8th European Software Engineering Conference, ACM, 2001, pp. 109–20, doi:10.1145/503209.503226.","short":"L. De Alfaro, T.A. Henzinger, in:, Proceedings of the 8th European Software Engineering Conference, ACM, 2001, pp. 109–120.","chicago":"De Alfaro, Luca, and Thomas A Henzinger. “Interface Automata.” In Proceedings of the 8th European Software Engineering Conference, 109–20. ACM, 2001. https://doi.org/10.1145/503209.503226.","ama":"De Alfaro L, Henzinger TA. Interface automata. In: Proceedings of the 8th European Software Engineering Conference. ACM; 2001:109-120. doi:10.1145/503209.503226","ista":"De Alfaro L, Henzinger TA. 2001. Interface automata. Proceedings of the 8th European software engineering conference. FSE: Foundations of Software Engineering, 109–120.","ieee":"L. De Alfaro and T. A. Henzinger, “Interface automata,” in Proceedings of the 8th European software engineering conference, Vienna, Austria, 2001, pp. 109–120.","apa":"De Alfaro, L., & Henzinger, T. A. (2001). Interface automata. In Proceedings of the 8th European software engineering conference (pp. 109–120). Vienna, Austria: ACM. https://doi.org/10.1145/503209.503226"},"publication":"Proceedings of the 8th European software engineering conference","article_processing_charge":"No","publication_identifier":{"isbn":["9781581133905"]},"day":"01","month":"06","scopus_import":"1","oa_version":"None","date_created":"2018-12-11T12:09:48Z","date_updated":"2023-05-08T12:01:02Z","author":[{"first_name":"Luca","last_name":"De Alfaro","full_name":"De Alfaro, Luca"},{"full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger"}],"publisher":"ACM","title":"Interface automata","publication_status":"published","status":"public","_id":"4622","acknowledgement":"We thank Edward A. Lee, Xiaojun Liu, Freddy Mang, and Yuhong Xiong for fruitful discussions. This research was supported in part by the AFOSR MURI grant F49620-00-1-0327, the DARPA MoBIES grant F33615-00-C-1703, the MARCO GSRC grant 98-DT-660, the NSF Theory grant CCR-9988172, and the NSF ITR grant CCR-0085949.","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","year":"2001","extern":"1","publist_id":"83","abstract":[{"text":"Conventional type systems specify interfaces in terms of values and domains. We present a light-weight formalism that captures the temporal aspects of software component interfaces. Specifically, we use an automata-based language to capture both input assumptions about the order in which the methods of a component are called, and output guarantees about the order in which the component calls external methods. The formalism supports automatic compatability checks between interface models, and thus constitutes a type system for component interaction. Unlike traditional uses of automata, our formalism is based on an optimistic approach to composition, and on an alternating approach to design refinement. According to the optimistic approach, two components are compatible if there is some environment that can make them work together. According to the alternating approach, one interface refines another if it has weaker input assumptions, and stronger output guarantees. We show that these notions have game-theoretic foundations that lead to efficient algorithms for checking compatibility and refinement.","lang":"eng"}],"type":"conference"},{"quality_controlled":"1","language":[{"iso":"eng"}],"doi":"10.1007/3-540-45449-7_11","conference":{"end_date":"2001-10-10","location":"Tahoe City, CA, USA","start_date":"2001-10-08","name":"EMSOFT: Embedded Software "},"publication_identifier":{"isbn":["9783540426738"]},"month":"09","publisher":"ACM","publication_status":"published","acknowledgement":"This research was supported in part by the AFOSR MURI grant F49620-00-1-0327, the DARPA ITO grant F33615-00-C-1693, the MARCO grant 98-DT-660, and the NSF ITR grant CCR-0085949.","year":"2001","volume":2211,"date_updated":"2023-05-08T12:11:20Z","date_created":"2018-12-11T12:09:48Z","author":[{"first_name":"Luca","last_name":"De Alfaro","full_name":"De Alfaro, Luca"},{"id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000−0002−2985−7724","first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A"}],"extern":"1","publist_id":"84","page":"148 - 165","citation":{"ama":"De Alfaro L, Henzinger TA. Interface theories for component-based design. In: Proceedings of the 1st International Workshop on Embedded Software. Vol 2211. ACM; 2001:148-165. doi:10.1007/3-540-45449-7_11","apa":"De Alfaro, L., & Henzinger, T. A. (2001). Interface theories for component-based design. In Proceedings of the 1st International Workshop on Embedded Software (Vol. 2211, pp. 148–165). Tahoe City, CA, USA: ACM. https://doi.org/10.1007/3-540-45449-7_11","ieee":"L. De Alfaro and T. A. Henzinger, “Interface theories for component-based design,” in Proceedings of the 1st International Workshop on Embedded Software, Tahoe City, CA, USA, 2001, vol. 2211, pp. 148–165.","ista":"De Alfaro L, Henzinger TA. 2001. Interface theories for component-based design. Proceedings of the 1st International Workshop on Embedded Software. EMSOFT: Embedded Software , LNCS, vol. 2211, 148–165.","short":"L. De Alfaro, T.A. Henzinger, in:, Proceedings of the 1st International Workshop on Embedded Software, ACM, 2001, pp. 148–165.","mla":"De Alfaro, Luca, and Thomas A. Henzinger. “Interface Theories for Component-Based Design.” Proceedings of the 1st International Workshop on Embedded Software, vol. 2211, ACM, 2001, pp. 148–65, doi:10.1007/3-540-45449-7_11.","chicago":"De Alfaro, Luca, and Thomas A Henzinger. “Interface Theories for Component-Based Design.” In Proceedings of the 1st International Workshop on Embedded Software, 2211:148–65. ACM, 2001. https://doi.org/10.1007/3-540-45449-7_11."},"publication":"Proceedings of the 1st International Workshop on Embedded Software","date_published":"2001-09-26T00:00:00Z","scopus_import":"1","article_processing_charge":"No","day":"26","intvolume":" 2211","title":"Interface theories for component-based design","status":"public","_id":"4623","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","oa_version":"None","alternative_title":["LNCS"],"type":"conference","abstract":[{"lang":"eng","text":"We classify component-based models of computation into component models and interface models. A component model specifies for each component howthe component behaves in an arbitrary environment; an interface model specifies for each component what the component expects from the environment. Component models support compositional abstraction, and therefore component-based verification. Interface models support compositional refinement, and therefore componentbased design. Many aspects of interface models, such as compatibility and refinement checking between interfaces, are properly viewed in a gametheoretic setting, where the input and output values of an interface are chosen by different players."}]},{"oa_version":"None","date_created":"2018-12-11T12:09:30Z","date_updated":"2023-05-09T12:23:16Z","author":[{"last_name":"Brown","first_name":"Timothy","full_name":"Brown, Timothy"},{"first_name":"Alessandro","last_name":"Pasetti","full_name":"Pasetti, Alessandro"},{"last_name":"Pree","first_name":"Wolfgang","full_name":"Pree, Wolfgang"},{"last_name":"Henzinger","first_name":"Thomas A","orcid":"0000−0002−2985−7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"},{"full_name":"Kirsch, Christoph","last_name":"Kirsch","first_name":"Christoph"}],"publisher":"IEEE","publication_status":"published","status":"public","title":"A reusable and platform-independent framework for distributed control systems","user_id":"ea97e931-d5af-11eb-85d4-e6957dddbf17","_id":"4564","acknowledgement":"This research was supported in part by DARPA under grants F336 15-C-98-36 14, F33615-00-(2-1693, and F33615-00-C-1703, and by MARC0 under grant 98-DT-660. ","year":"2001","extern":"1","publist_id":"143","abstract":[{"lang":"eng","text":"This paper presents a concept for integrating the embedded programming methodology Giotto and the object-oriented AOCS Framework to create an environment for the rapid development of distributed software for safety-critical embedded control systems with hard real-time requirements of the kind typically found in aerospace applications."}],"type":"conference","language":[{"iso":"eng"}],"doi":"10.1109/DASC.2001.964169","date_published":"2001-08-06T00:00:00Z","conference":{"start_date":"2001-10-14","location":"Daytona Beach, FL, USA","end_date":"2001-10-18","name":"DASC: Digital Avionics Systems Conference"},"page":"1 - 11","quality_controlled":"1","citation":{"short":"T. Brown, A. Pasetti, W. Pree, T.A. Henzinger, C. Kirsch, in:, Proceedings of the 20th Digital Avionics Systems Conference, IEEE, 2001, pp. 1–11.","mla":"Brown, Timothy, et al. “A Reusable and Platform-Independent Framework for Distributed Control Systems.” Proceedings of the 20th Digital Avionics Systems Conference, IEEE, 2001, pp. 1–11, doi:10.1109/DASC.2001.964169.","chicago":"Brown, Timothy, Alessandro Pasetti, Wolfgang Pree, Thomas A Henzinger, and Christoph Kirsch. “A Reusable and Platform-Independent Framework for Distributed Control Systems.” In Proceedings of the 20th Digital Avionics Systems Conference, 1–11. IEEE, 2001. https://doi.org/10.1109/DASC.2001.964169.","ama":"Brown T, Pasetti A, Pree W, Henzinger TA, Kirsch C. A reusable and platform-independent framework for distributed control systems. In: Proceedings of the 20th Digital Avionics Systems Conference. IEEE; 2001:1-11. doi:10.1109/DASC.2001.964169","ieee":"T. Brown, A. Pasetti, W. Pree, T. A. Henzinger, and C. Kirsch, “A reusable and platform-independent framework for distributed control systems,” in Proceedings of the 20th Digital Avionics Systems Conference, Daytona Beach, FL, USA, 2001, pp. 1–11.","apa":"Brown, T., Pasetti, A., Pree, W., Henzinger, T. A., & Kirsch, C. (2001). A reusable and platform-independent framework for distributed control systems. In Proceedings of the 20th Digital Avionics Systems Conference (pp. 1–11). Daytona Beach, FL, USA: IEEE. https://doi.org/10.1109/DASC.2001.964169","ista":"Brown T, Pasetti A, Pree W, Henzinger TA, Kirsch C. 2001. A reusable and platform-independent framework for distributed control systems. Proceedings of the 20th Digital Avionics Systems Conference. DASC: Digital Avionics Systems Conference, 1–11."},"publication":"Proceedings of the 20th Digital Avionics Systems Conference","publication_identifier":{"isbn":["0780370341"]},"article_processing_charge":"No","day":"06","month":"08","scopus_import":"1"}]