{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:27:11Z","timestamp":1754483231109},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540643562"},{"type":"electronic","value":"9783540697534"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0054173","type":"book-chapter","created":{"date-parts":[[2006,7,27]],"date-time":"2006-07-27T01:43:43Z","timestamp":1153964623000},"page":"201-216","source":"Crossref","is-referenced-by-count":11,"title":["Verification of large state\/event systems using compositionality and dependency analysis"],"prefix":"10.1007","author":[{"given":"J\u00d8rn","family":"Lind-Nielsen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Henrik Reif","family":"Andersen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gerd","family":"Behrmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Henrik","family":"Hulgaard","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"K\u00e5re","family":"Kristoifersen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kim G.","family":"Larsen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,5,25]]},"reference":[{"key":"14_CR1","doi-asserted-by":"crossref","unstructured":"H. R. Andersen, J. Staunstrup, and N. Maretti. Partial model checking with ROBDDs. In E. Brinksma, editor, Proceedings of TACAS'97, volume 1217 of LNCS, pages 35\u201349. Springer-Verlag, April 1997.","DOI":"10.1007\/BFb0035379"},{"key":"14_CR2","first-page":"398","volume-title":"Partial model checking (extended abstract)","author":"H.R. Andersen","year":"1995","unstructured":"H.R. Andersen. Partial model checking (extended abstract). In Proceedings, Tenth Annual IEEE Symposium on Logic in Computer Science, pages 398\u2013407, La Jolla, San Diego, 26\u201329 July 1995. IEEE Computer Society Press."},{"key":"14_CR3","first-page":"156","volume-title":"Model checking large software specifications","author":"R.J. Anderson","year":"1996","unstructured":"R.J. Anderson, P. Beame, S. M. Burns, W. Chan, F. Modugno, D. Notkin, and J.D. Reese. Model checking large software specifications. In D. Garlan, editor, SIGSOFT '96. Proceedings of the Fourth ACM SIGSOFT Symposium on the Foundations of Software Engineering, pages 156\u201366, San Francisco, 1996. ACM."},{"key":"14_CR4","first-page":"29","volume-title":"LNCS","author":"F. Balarin","year":"1993","unstructured":"F. Balarin and A.L. Sangiovanni-Vincentelli. An iterative approach to language containment. In C. Courcoubetis, editor, CAV'93. 5th International Conference on Computer Aided Verification, volume 697 of LNCS, pages 29\u201340, Berlin, 1993. Springer-Verlag."},{"issue":"C-35","key":"14_CR5","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"8","author":"R.E. Bryant","year":"1986","unstructured":"R.E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, 8(C-35):677\u2013691, 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"14_CR6","unstructured":"J. R. Burch, E. M. Clarke, and D. E. Long. Symbolic model checking with partitioned transition relations. In A. Halaas and P. B. Denyer, editors, Proc. 1991 Int. Conf. on VLSI, August 1991."},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. In Proceedings, Fifth Annual IEEE Symposium on Logic in Computer Science, pages 428\u2013439. IEEE Computer Society Press, 1990.","DOI":"10.1109\/LICS.1990.113767"},{"issue":"4","key":"14_CR8","doi-asserted-by":"publisher","first-page":"401","DOI":"10.1109\/43.275352","volume":"13","author":"J.R. Burch","year":"1994","unstructured":"J.R. Burch, E.M. Clarke, D.E. Long, K.L. McMillan, and D.L. Dill. Symbolic model checking for sequential circuit verification. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 13(4):401\u2013424, 1994.","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"issue":"2","key":"14_CR9","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"E.M. Clarke, E.A. Emerson, and A.P. Sistla. Automatic verification of finitestate concurrent systems using temporal logic specifications. A CM Transactions on Programming Languages and Systems, 8(2):244\u2013263, 1986.","journal-title":"A CM Transactions on Programming Languages and Systems"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, O. Grumberg, and D.E. Long. Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 1994.","DOI":"10.1145\/186025.186051"},{"key":"14_CR11","first-page":"353","volume-title":"Compositional model checking","author":"E.M. Clarke","year":"1989","unstructured":"E.M. Clarke, D.E. Long, and K.L. McMillan. Compositional model checking. In Proceedings, Fourth Annual Symposium on Logic in Computer Science, pages 353\u2013362, Asilomar Conference Center, Pacific Grove, California, June 5\u20138 1989. IEEE Computer Society Press."},{"key":"14_CR12","doi-asserted-by":"crossref","unstructured":"O. Coudert, C. Berthet, and J. C. Madre. Verification of synchronous sequential machines based on symbolic execution. In J. Sifakis, editor, Automatic Verification Methods for Finite State Systems. Proceedings, volume 407 of LNCS, pages 365\u2013373. Springer-Verlag, 1989.","DOI":"10.1007\/3-540-52148-8_30"},{"key":"14_CR13","first-page":"75","volume-title":"Verifying temporal properties of sequential machines without building their state diagrams","author":"O. Coudert","year":"1990","unstructured":"O. Coudert, J. C. Madre, and C. Berthet. Verifying temporal properties of sequential machines without building their state diagrams. In E.M. Clarke and R.P. Kurshan, editors, CAV'90. Workshop on Computer-Aided Verification., pages 75\u201384, Rutgers, New Jersey, 1990. American Mathematical Society."},{"key":"14_CR14","first-page":"299","volume-title":"LNCS","author":"D. Geist","year":"1994","unstructured":"D. Geist and I. Beer. Efficient model checking by automated ordering of transition relation partitions. In D.L. Dill, editor, CAV'94-6th International Conference on Computer Aided Verification, volume 818 of LNCS, pages 299\u2013310, Stanford, 1994. Springer-Verlag."},{"issue":"3","key":"14_CR15","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D. Harel","year":"1987","unstructured":"David Harel. STATECHARTS: A visual formalism for complex systems. Science of Computer Programming, 8(3):231\u2013274, June 1987.","journal-title":"Science of Computer Programming"},{"key":"14_CR16","doi-asserted-by":"crossref","unstructured":"K. J. Kristoffersen, F. Laroussinie, K. G. Larsen, P. Patterson, and W. Yi. A compositional proof of a read-time mutual exclusion protocol. In M. Bidoit and M. Dauchet, editors, Proceedings of TAPSOFT '97: Theory and Practice of Software Development, volume 1214 of LNCS, pages 565\u2013579. Springer-Verlag, 1997.","DOI":"10.1007\/BFb0030626"},{"key":"14_CR17","first-page":"76","volume-title":"Tearing based automatic abstraction for CTL model checking","author":"W. Lee","year":"1996","unstructured":"W. Lee, A. Pardo, J.-Y. Jang, G. Hachtel, and F. Somenzi. Tearing based automatic abstraction for CTL model checking. In 1996 IEEE\/ACM International Conference on Computer-Aided Design, pages 76\u201381, San Jose, CA, 1996. IEEE Comput. Soc. Press."},{"key":"14_CR18","unstructured":"Beologic\u00ae A\/S. visualSTATE\u2133 3.0 User's Guide, 1996."},{"key":"14_CR19","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, Norwell Massachusetts, 1993."},{"key":"14_CR20","first-page":"77","volume-title":"Feasibility of model checking software requirements: a case study","author":"T. Sreemani","year":"1996","unstructured":"T. Sreemani and J.M. Atlee. Feasibility of model checking software requirements: a case study. In COMPASS '96. Proceedings of the Eleventh Annual Conference on Computer Assurance, pages 77\u201388, New York, USA, 1996. IEEE."}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0054173","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,20]],"date-time":"2019-04-20T04:27:52Z","timestamp":1555734472000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0054173"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540643562","9783540697534"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/bfb0054173","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}