{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,15]],"date-time":"2025-08-15T00:28:42Z","timestamp":1755217722200,"version":"3.43.0"},"reference-count":24,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2001,1,1]],"date-time":"2001-01-01T00:00:00Z","timestamp":978307200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Formal Methods in System Design"],"published-print":{"date-parts":[[2001,1]]},"DOI":"10.1023\/a:1008736219484","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T11:37:32Z","timestamp":1040557052000},"page":"5-23","source":"Crossref","is-referenced-by-count":17,"title":["Verification of Large State\/Event Systems Using Compositionality and Dependency Analysis"],"prefix":"10.1007","volume":"18","author":[{"given":"J\u00f8rn","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":"Henrik","family":"Hulgaard","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gerd","family":"Behrmann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"K\u00e5re","family":"Kristoffersen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kim G.","family":"Larsen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"281737_CR1","doi-asserted-by":"crossref","unstructured":"H. Andersen, \u201cPartial model checking (extended abstract),\u201d in Proceedings; Tenth Annual IEEE Symposium on Logic in Computer Science, La Jolla, San Diego, 1995, pp. 398\u2013407.","DOI":"10.1109\/LICS.1995.523274"},{"key":"281737_CR2","doi-asserted-by":"crossref","unstructured":"H.R. Andersen, J. Staunstrup, and N. Maretti, \u201cPartial model checking with ROBDDs,\u201d in E. Brinksma (Ed.), Proceedings of TACAS'97, Vol. 1217 of LNCS, 1997, pp. 35\u201349.","DOI":"10.1007\/BFb0035379"},{"key":"281737_CR3","doi-asserted-by":"crossref","unstructured":"R. Anderson, P. Beame, S.M. Burns, W. Chan, F. Modugno, D. Notkin, and J. Reese, \u201cModel checking large software specifications,\u201d in D. Garlan (Ed.), SIGSOFT '96, Proceedings of the Fourth ACM SIGSOFT Symposium on the Foundations of Software Engineering, San Francisco, 1996, pp. 156\u2013166.","DOI":"10.1145\/239098.239127"},{"key":"281737_CR4","doi-asserted-by":"crossref","first-page":"29","DOI":"10.1007\/3-540-56922-7_4","volume-title":"CAV'93, 5th International Conference on Computer Aided Verification","author":"F. Balarin","year":"1993","unstructured":"F. Balarin and A. Sangiovanni-Vincentelli, \u201cAn iterative approach to language containment,\u201d in C. Courcoubetis (Ed.), CAV'93, 5th International Conference on Computer Aided Verification, Vol. 697 of LNCS, Berlin, 1993, pp. 29\u201340."},{"key":"281737_CR5","first-page":"163","volume-title":"TACAS: Tools and Algorithms for the Construction and Analysis of Systems","author":"G. Behrmann","year":"1999","unstructured":"G. Behrmann, K.G. Larsen, H.R. Andersen, H. Hulgaard, and J. Lind-Nielsen, \u201cVerification of hierarchical state\/event systems using reusability and compositionality,\u201d in TACAS: Tools and Algorithms for the Construction and Analysis of Systems, Springer-Verlag, Amsterdam, The Netherlands, 1999, pp. 163\u2013172."},{"issue":"C-35","key":"281737_CR6","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"8","author":"R. Bryant","year":"1986","unstructured":"R. Bryant, \u201cGraph-based algorithms for Boolean function manipulation,\u201d IEEE Transactions on Computers, Vol. 8, No. C-35, pp. 677\u2013691, 1986.","journal-title":"IEEE Transactions on Computers"},{"issue":"4","key":"281737_CR7","doi-asserted-by":"crossref","first-page":"401","DOI":"10.1109\/43.275352","volume":"13","author":"J. Burch","year":"1994","unstructured":"J. Burch, E. Clarke, D. Long, K. McMillan, and D. Dill, \u201cSymbolic model checking for sequential circuit verification,\u201d IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. 13, No. 4, pp. 401\u2013424, 1994.","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"281737_CR8","unstructured":"J.R. Burch, E.M. Clarke, and D.E. Long, \u201cSymbolic model checking with partitioned transition relations,\u201d in A. Halaas and P.B. Denyer (Eds.), Proc. 1991 Int. Conf. on VLSI, 1991."},{"key":"281737_CR9","doi-asserted-by":"crossref","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang, \u201cSymbolic model checking: 1020 states and beyond,\u201d in Proceedings; Fifth Annual IEEE Symposium on Logic in Computer Science, 1990, pp. 428\u2013439.","DOI":"10.1109\/LICS.1990.113767"},{"key":"281737_CR10","doi-asserted-by":"crossref","unstructured":"E. Clarke, O. Grumberg, and D. Long, \u201cModel checking and abstraction,\u201d ACMTransactions on Programming Languages and Systems, 1994.","DOI":"10.1145\/186025.186051"},{"key":"281737_CR11","doi-asserted-by":"crossref","first-page":"353","DOI":"10.1109\/LICS.1989.39190","volume-title":"Proceedings, Fourth Annual Symposium on Logic in Computer Science","author":"E. Clarke","year":"1989","unstructured":"E. Clarke, D. Long, and K. McMillan, \u201cCompositional model checking,\u201d in Proceedings, Fourth Annual Symposium on Logic in Computer Science, Asilomar Conference Center, Pacific Grove, California, 1989, pp. 353\u2013362."},{"key":"281737_CR12","doi-asserted-by":"crossref","unstructured":"O. Coudert, C. Berthet, and J.C. Madre, \u201cVerification of synchronous sequential machines based on symbolic execution,\u201d in J. Sifakis (Ed.), Automatic Verification Methods for Finite State Systems Proceedings, Vol. 407 of LNCS, 1989, pp. 365\u2013373.","DOI":"10.1007\/3-540-52148-8_30"},{"key":"281737_CR13","first-page":"75","volume-title":"CAV'90,Workshop on Computer-Aided Verification","author":"O. Coudert","year":"1990","unstructured":"O. Coudert, J.C. Madre, and C. Berthet,\u201cVerifying temporal properties of sequential machines without building their state diagrams,\u201d in E. Clarke and R. Kurshan (Eds.), CAV'90,Workshop on Computer-Aided Verification. Rutgers, New Jersey, 1990, pp. 75\u201384."},{"key":"281737_CR14","doi-asserted-by":"crossref","first-page":"299","DOI":"10.1007\/3-540-58179-0_63","volume-title":"CAV'94; 6th International Conference on Computer Aided Verification","author":"D. Geist","year":"1994","unstructured":"D. Geist and I. Beer, \u201cEfficient model checking by automated ordering of transition relation partitions,\u201d in D. Dill (Ed.), CAV'94; 6th International Conference on Computer Aided Verification, Vol.818 of LNCS, Stanford, 1994, pp. 299\u2013310."},{"issue":"3","key":"281737_CR15","doi-asserted-by":"crossref","first-page":"231","DOI":"10.1016\/0167-6423(87)90035-9","volume":"8","author":"D. Harel","year":"1987","unstructured":"D. Harel, \u201cSTATECHARTS: A visual formalism for complex systems,\u201d Science of Computer Programming, Vol. 8, No. 3, pp. 231\u2013274, 1987.","journal-title":"Science of Computer Programming"},{"key":"281737_CR16","doi-asserted-by":"crossref","unstructured":"K.J. Kristoffersen, F. Laroussinie, K.G. Larsen, P. Patterson, and W. Yi, \u201cA compositional proof of a read-time mutual exclusion protocol,\u201d in M. Bidoit and M. Dauchet (Eds.), Proceedings of TAPSOFT '97: Theory and Practice of Software Development, Vol. 1214 of LNCS, 1997, pp. 565\u2013579.","DOI":"10.1007\/BFb0030626"},{"key":"281737_CR17","unstructured":"W. Lee, A. Pardo, J.-Y. Jang, G. Hachtel, and F. Somenzi, \u201cTearing based automatic abstraction for CTL model checking,\u201d in 1996 IEEE\/ACM International Conference on Computer-Aided Design, San Jose, CA, 1996, pp. 76\u201381."},{"issue":"9","key":"281737_CR18","doi-asserted-by":"crossref","first-page":"684","DOI":"10.1109\/32.317428","volume":"20","author":"N.G. Leveson","year":"1994","unstructured":"N.G. Leveson, M.P.E. Heimdahl, H. Hildreth, and J.D. Reese, \u201cRequirement specification for process-control systems,\u201d IEEE Transactions on Software Engineering, Vol. 20, No. 9, 1994, pp. 684\u2013706.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"281737_CR19","unstructured":"J. Lind-Nielsen, \u201cBuDDy: Binary decision diagram package,\u201d www.itu.dk\/research\/buddy, 1999."},{"key":"281737_CR20","first-page":"316","volume":"1633","author":"J. Lind-Nielsen","year":"1999","unstructured":"J. Lind-Nielsen and H.R. Andersen, \u201cStepwise CTL model checking of state\/event systems,\u201d in CAV'99. 11th International Conference on Computer Aided Verification, Vol. 1633 of LNCS, 1999, pp. 316\u2013327.","journal-title":"CAV'99. 11th International Conference on Computer Aided Verification"},{"key":"281737_CR21","unstructured":"Beologicr A\/S, \u201cvisualSTATETM 3.0 User's Guide,\u201d 1996."},{"key":"281737_CR22","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K. McMillan","year":"1993","unstructured":"K. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell Massachusetts, 1993."},{"key":"281737_CR23","doi-asserted-by":"crossref","unstructured":"A. Pardo and G.D. Hachtel, \u201cAutomatic abstraction techniques for propositional \u03bc-calculus model checking,\u201d in O. Grumberg (Ed.), CAV'97, 9th International Conference on Computer Aided Verification, Vol. 1254 of LNCS, 1997, pp. 12\u201323.","DOI":"10.1007\/3-540-63166-6_5"},{"key":"281737_CR24","unstructured":"T. Sreemani and J. Atlee, \u201cFeasibility of model checking software requirements: a case study,\u201d in COMPASS '96, Proceedings of the Eleventh Annual Conference on Computer Assurance, New York, USA, 1996, pp. 77\u201388."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008736219484.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1008736219484\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008736219484.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T19:10:17Z","timestamp":1754421017000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1008736219484"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,1]]},"references-count":24,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2001,1]]}},"alternative-id":["281737"],"URL":"https:\/\/doi.org\/10.1023\/a:1008736219484","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2001,1]]}}}