{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T13:53:09Z","timestamp":1754488389815},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540581796"},{"type":"electronic","value":"9783540484691"}],"license":[{"start":{"date-parts":[[1994,1,1]],"date-time":"1994-01-01T00:00:00Z","timestamp":757382400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58179-0_75","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T15:25:47Z","timestamp":1330269947000},"page":"455-467","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":12,"title":["Model checking using adaptive state and data abstraction"],"prefix":"10.1007","author":[{"given":"Dennis","family":"Dams","sequence":"first","affiliation":[]},{"given":"Rob","family":"Gerth","sequence":"additional","affiliation":[]},{"given":"Gert","family":"D\u00f6hmen","sequence":"additional","affiliation":[]},{"given":"Ronald","family":"Herrmann","sequence":"additional","affiliation":[]},{"given":"Peter","family":"Kelb","sequence":"additional","affiliation":[]},{"given":"Hergen","family":"Pargmann","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"37_CR1","unstructured":"J. R. Burch, E. M. Clarke, K. L. Mcmillan, D. L. Dill, and J. Hwang. Symbolic model checking: 1020 states and beyond. In Proceedings of the Fifth Anual IEEE Symposium on Logic in Computer Science (LICS), 1990."},{"issue":"3","key":"37_CR2","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1016\/0167-6423(92)90018-7","volume":"18","author":"A. Bouajjani","year":"1992","unstructured":"A. Bouajjani, J.-C. Fernandez, N. Halbwachs, P. Raymond, and C. Ratel. Minimal state graph generation. Science of Computer Programmming, 18(3):247\u2013271, 1992.","journal-title":"Science of Computer Programmming"},{"key":"37_CR3","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. E. Bryant","year":"1986","unstructured":"R. E. Bryant. Graph-based algorithms for boolean function manipulation. Transactions on Computers, C-35:677\u2013691, 1986.","journal-title":"Transactions on Computers"},{"issue":"3","key":"37_CR4","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"R. E. Bryant","year":"1992","unstructured":"R. E. Bryant. Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys, 24(3):293\u2013318, 1992.","journal-title":"ACM Computing Surveys"},{"key":"37_CR5","doi-asserted-by":"crossref","unstructured":"P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by constructing or approximation of fixed points. In Proceedings of the Fourth Annual ACM Symposium on Principles of Programming Languages (POPL), pages 238\u2013252. ACM, 1977.","DOI":"10.1145\/512950.512973"},{"key":"37_CR6","doi-asserted-by":"crossref","unstructured":"D. Dams, R. Gerth, and O. Grumberg. Generation of reduced models for checking fragments of CTL. In C. Courcoubetis, editor, Proceedings of the Fifth Conference on Computer-Aided Verification, volume 697 of Lecture Notes in Computer Science. Springer-Verlag, 1993.","DOI":"10.1007\/3-540-56922-7_39"},{"key":"37_CR7","unstructured":"D. Dams, O. Grumberg, and R. Gerth. Abstract interpretation of reactive systems: abstractions preserving \u2200CTL*, \u2203CTL* and CTL*. In Proceedings of PROCOMET, IFIP. North-Holland, 1994. To appear."},{"key":"37_CR8","unstructured":"R. Gerth, R. Kuiper, D. Peled, and W. Penczek. A partial order approach to branching time logic model checking, 1994. Submitted."},{"key":"37_CR9","unstructured":"P. Godefroid and P. Wolper. A partial approach to model checking. In Proceedings of the Sixth Anual IEEE Symposium on Logic in Computer Science (LICS), 1991."},{"key":"37_CR10","doi-asserted-by":"crossref","unstructured":"D. Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8, 1987.","DOI":"10.1016\/0167-6423(87)90035-9"},{"key":"37_CR11","unstructured":"J. Helbig and P. Kelb. An OBDD representation of statecharts, 1994. To appear in EDAC94."},{"key":"37_CR12","doi-asserted-by":"crossref","first-page":"571","DOI":"10.1016\/0165-6074(93)90197-S","volume":"38","author":"J. Helbig","year":"1993","unstructured":"J. Helbig, R. Schl\u00f6r, W. Damm, G. D\u00f6hmen, and P. Kelb. VHDL\/S\u2014integrating statecharts, timing diagrams and VHDL. Microprocessing and Microprogramming, 38:571\u2013580, 1993.","journal-title":"Microprocessing and Microprogramming"},{"key":"37_CR13","doi-asserted-by":"crossref","unstructured":"D. Peled. All from one, one for all, on model-checking using representatives. In Proceedings of the Fifth International Conference on Computer-Aided Verification, Lecture Notes in Computer Science, pages 409\u2013423. Springer-Verlag, 1993.","DOI":"10.1007\/3-540-56922-7_34"},{"key":"37_CR14","unstructured":"R. Schl\u00f6r and W. Damm. Specification and verification of system-level hardware designs using timing diagrams. In EDAC93, 1993."},{"key":"37_CR15","doi-asserted-by":"crossref","unstructured":"A. Valmari. A stubborn attack on state explosion. In Proceedings of the Second Conference on Computer-Aided Verification, Lecture Notes in Computer Science. Springer-Verlag, 1991.","DOI":"10.1090\/dimacs\/003\/04"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58179-0_75","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,9]],"date-time":"2020-01-09T02:22:56Z","timestamp":1578536576000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58179-0_75"}},"subtitle":["Extended abstract"],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540581796","9783540484691"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-58179-0_75","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]},"assertion":[{"value":"7 June 2005","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}