{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T19:49:10Z","timestamp":1762458550517},"publisher-location":"Berlin, Heidelberg","reference-count":9,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439974"},{"type":"electronic","value":"9783540456575"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45657-0_25","type":"book-chapter","created":{"date-parts":[[2007,5,19]],"date-time":"2007-05-19T14:59:43Z","timestamp":1179586783000},"page":"338-342","source":"Crossref","is-referenced-by-count":11,"title":["Exploiting Behavioral Hierarchy for Efficient Model Checking"],"prefix":"10.1007","author":[{"given":"Rajeev","family":"Alur","sequence":"first","affiliation":[]},{"given":"Michael","family":"McDougall","sequence":"additional","affiliation":[]},{"given":"Zijiang","family":"Yang","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,9,20]]},"reference":[{"key":"25_CR1","doi-asserted-by":"crossref","unstructured":"R. Alur and R. Grosu. Modular refinement of hierarchic reactive machines. In Proc. 27th POPL, pages 390\u2013402, 2000.","DOI":"10.1145\/325694.325746"},{"key":"25_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1007\/10722167_23","volume-title":"Proc. 12th CAV","author":"R. Alur","year":"2000","unstructured":"R. Alur, R. Grosu, and M. McDougall. Efficient reachability analysis of hierarchical reactive machines. In Proc. 12th CAV, LNCS 1855, pages 280\u2013295, 2000."},{"key":"25_CR3","doi-asserted-by":"crossref","first-page":"260","DOI":"10.1007\/3-540-44585-4_25","volume-title":"Computer Aided Verification","author":"Thomas Ball","year":"2001","unstructured":"T. Ball and S. Rajamani. The SLAM toolkit. In Proc. 13th CAV, 2001."},{"key":"25_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"428","DOI":"10.1007\/3-540-61474-5_95","volume-title":"Proc. 8th CAV","author":"R. Brayton","year":"1996","unstructured":"R. Brayton, G. Hachtel, A. Sangiovanni-Vincentell, F. Somenzi, et. al. VIS: A system for verification and synthesis. In Proc. 8th CAV, LNCS 1102, pages 428\u2013432, 1996."},{"issue":"7","key":"25_CR5","doi-asserted-by":"publisher","first-page":"498","DOI":"10.1109\/32.708566","volume":"24","author":"W. Chan","year":"1998","unstructured":"W. Chan, R. Anderson, P. Beame, S. Burns, F. Modugno, D. Notkin, and J. Reese. Model checking large software specifications. IEEE Trans. on Software Engg., 24(7):498\u2013519, 1998.","journal-title":"IEEE Trans. on Software Engg."},{"key":"25_CR6","doi-asserted-by":"crossref","unstructured":"J. Corbett, M. Dwyer, J. Hatcliff, S. Laubach, C. Pasareanu, Robby, and H. Zheng. Bandera: Extracting finite-state models from Java source code. In Proc. 22nd ICSE, pages 439\u2013448. 2000.","DOI":"10.1145\/337180.337234"},{"key":"25_CR7","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D. Harel","year":"1987","unstructured":"D. Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8:231\u2013274, 1987.","journal-title":"Science of Computer Programming"},{"issue":"5","key":"25_CR8","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G. Holzmann","year":"1997","unstructured":"G. Holzmann. The model checker SPIN. IEEE Trans. on Software Engg., 23(5):279\u2013295, 1997.","journal-title":"IEEE Trans. on Software Engg."},{"key":"25_CR9","doi-asserted-by":"crossref","unstructured":"K. McMillan. Symbolic model checking: an approach to the state explosion problem. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45657-0_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T05:21:08Z","timestamp":1556428868000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45657-0_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439974","9783540456575"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/3-540-45657-0_25","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}