{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T22:04:39Z","timestamp":1725573879600},"publisher-location":"Berlin, Heidelberg","reference-count":21,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540204619"},{"type":"electronic","value":"9783540398936"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2003]]},"DOI":"10.1007\/978-3-540-39893-6_32","type":"book-chapter","created":{"date-parts":[[2011,1,7]],"date-time":"2011-01-07T15:35:57Z","timestamp":1294414557000},"page":"560-578","source":"Crossref","is-referenced-by-count":0,"title":["Compositional Verification of a Switch Fabric from Nortel Networks"],"prefix":"10.1007","author":[{"given":"Hong","family":"Peng","sequence":"first","affiliation":[]},{"given":"Sofi\u00e8ne","family":"Tahar","sequence":"additional","affiliation":[]},{"given":"Yassine","family":"Mokhtari","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"32_CR1","doi-asserted-by":"crossref","unstructured":"Arora, A., Attie, P.C., Emerson, E.A.: Synthesis of fault-tolerant concurrent programs. In: Proceedings of the 17th Annual ACM Symposium on Principles of Distributed Computing, Puerto Vallarta, Mexico, June 1998, pp. 173\u2013182 (1998)","DOI":"10.1145\/277697.277729"},{"key":"32_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"428","DOI":"10.1007\/3-540-61474-5_95","volume-title":"Computer Aided Verification","author":"R.K. Brayton","year":"1996","unstructured":"Brayton, R.K., et al.: VIS: A system for verification and synthesis. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 428\u2013432. Springer, Heidelberg (1996)"},{"key":"32_CR3","unstructured":"Cadence Design Systems. Technical manual of FormalCheck, v2.3 edn. (1987-1999)"},{"issue":"5","key":"32_CR4","doi-asserted-by":"publisher","first-page":"1512","DOI":"10.1145\/186025.186051","volume":"16","author":"E.M. Clarke","year":"1994","unstructured":"Clarke, E.M., Grumberg, O., Long, D.: Model checking and abstraction. ACM Transactions on Programming Languages and Systems\u00a016(5), 1512\u20131542 (1994)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"32_CR5","doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Los Angeles, California, USA, pp. 238\u2013252 (1977)","DOI":"10.1145\/512950.512973"},{"issue":"3","key":"32_CR6","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"E.A. Emerson","year":"1982","unstructured":"Emerson, E.A., Clarke, E.M.: Using branching time temporal logic to synthesize synchronization skeletons. Science of Computer Programming\u00a02(3), 241\u2013266 (1982)","journal-title":"Science of Computer Programming"},{"issue":"3","key":"32_CR7","doi-asserted-by":"publisher","first-page":"843","DOI":"10.1145\/177492.177725","volume":"16","author":"O. Grumberg","year":"1994","unstructured":"Grumberg, O., Long, D.E.: Model checking and modular verification. ACM Transactions on Programming Languages and Systems\u00a016(3), 843\u2013871 (1994)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"32_CR8","volume-title":"Design and validation of computer protocols","author":"G.J. Holzmann","year":"1991","unstructured":"Holzmann, G.J.: Design and validation of computer protocols. Prentice-Hall, Englewood Cliffs (1991)"},{"key":"32_CR9","doi-asserted-by":"crossref","unstructured":"Kesten, Y., Pnueli, A.: Modularization and abstraction: the key to practical formal verification. In: 23rd Int. Symp. Mathematical Foundations of Computer Science, Brno, Czech Republic (1998)","DOI":"10.1007\/BFb0055757"},{"key":"32_CR10","volume-title":"Computer-aided verification of coordinating processes","author":"R.P. Kurshan","year":"1994","unstructured":"Kurshan, R.P.: Computer-aided verification of coordinating processes. Princeton University Press, Princeton (1994)"},{"key":"32_CR11","unstructured":"Long, D.E.: Model Checking, Abstraction, and Compositional Verification. PhD thesis, CMU (1993)"},{"key":"32_CR12","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Safety","author":"Z. Manna","year":"1991","unstructured":"Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Safety. Springer, New York (1991)"},{"key":"32_CR13","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer, Dordrecht (1993)"},{"key":"32_CR14","volume-title":"Proceeding of IEEE International Conference on Computer Design","author":"H. Peng","year":"2002","unstructured":"Peng, H., Mokhtari, Y., Tahar, S.: Environment synthesis for compositional model checking. In: Proceeding of IEEE International Conference on Computer Design, Freiburg, Germany. IEEE computer society Press, Los Alamitos (September 2002)"},{"key":"32_CR15","series-title":"Lecture Notes in Computer Science","first-page":"433","volume-title":"Computer Aided Verification","author":"K.S. Namjoshi","year":"2000","unstructured":"Namjoshi, K.S., Kurshan, R.P.: Syntactic program transformations for automatic abstraction. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 433\u2013449. Springer, Heidelberg (2000)"},{"key":"32_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/3-540-48234-2_14","volume-title":"Theoretical and Practical Aspects of SPIN Model Checking","author":"C.S. Pasareanu","year":"1999","unstructured":"Pasareanu, C.S., Dwyer, M.B., Huth, M.: Assume-guarantee model checking of software: A comparative case study. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol.\u00a01680, pp. 168\u2013183. Springer, Heidelberg (1999)"},{"key":"32_CR17","doi-asserted-by":"crossref","unstructured":"Peng, H., Mokhtari, Y., Tahar, S.: Model reduction based on value dependency. In: Proceeding of IEEE International ASIC\/SOC Conference, Washigton, DC, USA (September 2001)","DOI":"10.1109\/ASIC.2001.954701"},{"key":"32_CR18","unstructured":"Peng, H., Tahar, S.: Compositional verification of IP based designs. In: Proceedings of IFIP International Workshop on IP Based Synthesis and System Design, Grenoble, France (December 1999)"},{"key":"32_CR19","series-title":"NATO ASI series. Series F","volume-title":"Logics and Models of Concurrent Systems","author":"A. Pnueli","year":"1984","unstructured":"Pnueli, A.: In transition for global to modular temporal reasoning about programs. In: Kurshan, K.R. (ed.) Logics and Models of Concurrent Systems. NATO ASI series. Series F, vol.\u00a013. Springer, Heidelberg (1984)"},{"key":"32_CR20","unstructured":"Northern Telecom. Specification of a 4*4 ATM switch (November 1998)"},{"key":"32_CR21","unstructured":"Yorav, K.: Exploiting syntactic structure for automatic verification. PhD thesis, Israel institute of technology (June 2000)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-39893-6_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,23]],"date-time":"2019-03-23T09:16:48Z","timestamp":1553332608000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-39893-6_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003]]},"ISBN":["9783540204619","9783540398936"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-39893-6_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2003]]}}}