{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,8]],"date-time":"2025-01-08T05:31:58Z","timestamp":1736314318124,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540627906"},{"type":"electronic","value":"9783540685197"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/bfb0035380","type":"book-chapter","created":{"date-parts":[[2006,1,25]],"date-time":"2006-01-25T15:28:40Z","timestamp":1138202920000},"page":"50-64","source":"Crossref","is-referenced-by-count":8,"title":["Space efficient reachability analysis through use of pseudo-root states"],"prefix":"10.1007","author":[{"given":"Atanas N.","family":"Parashkevov","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jay","family":"Yantchev","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,26]]},"reference":[{"issue":"8","key":"5_CR1","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. IEEE Trans. Computers, C-35(8):677\u2013691, August 1986.","journal-title":"IEEE Trans. Computers"},{"issue":"3","key":"5_CR2","doi-asserted-by":"crossref","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, September 1992.","journal-title":"ACM Computing Surveys"},{"issue":"4","key":"5_CR3","doi-asserted-by":"crossref","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 Trans. on Computer Aided Design of Integrated Circuits and Systems, 13(4):401\u2013424, 1994.","journal-title":"IEEE Trans. on Computer Aided Design of Integrated Circuits and Systems"},{"key":"5_CR4","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J. R. Burch","year":"1992","unstructured":"J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 10 20 states and beyond. Information and Computation, 98: 142\u2013170, 1992.","journal-title":"Information and Computation"},{"key":"5_CR5","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1145\/356850.356854","volume":"13","author":"J. Cohen","year":"1981","unstructured":"J. Cohen. Garbage collection of linked data structures. ACM Computing Surveys, 13:341\u2013367, 1981.","journal-title":"ACM Computing Surveys"},{"key":"5_CR6","unstructured":"Formal Systems (Europe) Ltd. FDR2 User Manual, August 1996."},{"key":"5_CR7","volume-title":"PhD thesis","author":"P. Godefroid","year":"1994","unstructured":"P. Godefroid. Partial-order methods for the verification of concurrent systems. PhD thesis, University of Li\u00e8ge, Belgium, 1994."},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"P. Godefroid, G. J. Holzmann, and D. Pirottin. State space caching revisited. In CAV '92, pages 178\u2013191. Lecture Notes in Computer Science, 663, Springer Verlag, 1992.","DOI":"10.1007\/3-540-56496-9_15"},{"issue":"3","key":"5_CR9","first-page":"117","volume":"11","author":"P. H. Hartel","year":"1990","unstructured":"P. H. Hartel. Comparison of three garbage collection algorithms. Structured Programming, 11(3):117\u2013128, 1990.","journal-title":"Structured Programming"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"C. A. R. Hoare. Communicating Sequential Processes. Prentice Hall, 1985.","DOI":"10.1007\/978-3-642-82921-5_4"},{"issue":"6","key":"5_CR11","doi-asserted-by":"crossref","first-page":"683","DOI":"10.1109\/TSE.1987.233206","volume":"13","author":"G. J. Holzmann","year":"1987","unstructured":"G. J. Holzmann. Automated protocol validation in Argos: Assertion proving and scatter searching. IEEE Trans. on Software Engineering, 13(6):683\u2013696, 1987.","journal-title":"IEEE Trans. on Software Engineering"},{"issue":"2","key":"5_CR12","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1002\/spe.4380180203","volume":"18","author":"G. J. Holzmann","year":"1988","unstructured":"G. J. Holzmann. An improved protocol reachability analysis technique. Software \u2014 Practice and Experience, 18(2):137\u2013161, 1988.","journal-title":"Software \u2014 Practice and Experience"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"C. Jard and T. J\u00e9ron. Bounded-memory algorithms for verification on-the-fly. In CAV '91, pages 192\u2013202. Lecture Notes in Computer Science, 575, Springer Verlag, 1991.","DOI":"10.1007\/3-540-55179-4_19"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"K. L. McMillan. Symbolic Model Checking \u2014 an approach to the state explosion problem. PhD thesis, School of Computer Science, Carnegie Mellon University, 1992.","DOI":"10.1007\/978-1-4615-3190-6_3"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"H. Miller and S. Katz. Saving space by fully exploiting invisible transitions. In CAV '96, pages 336\u2013347. Lecture Notes in Computer Science, 1102, Springer Verlag, 1996.","DOI":"10.1007\/3-540-61474-5_81"},{"key":"5_CR16","unstructured":"R. Milner. Communication and Concurrency. Prentice Hall, 1989."},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"A. N. Parashkevov and J. Yantchev. ARC \u2014 a tool for efficient refinement and equivalence checking for CSP. In IEEE Int. Conf. on Algorithms and Architectures for Parallel Processing ICA3PP '96, pages 68\u201375, 1996.","DOI":"10.1109\/ICAPP.1996.562859"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"D. Peled. Combining partial order reductions with on-the-fly model-checking. In CAV '94, pages 377\u2013390. Lecture Notes in Computer Science, 818, Springer Verlag, 1994.","DOI":"10.1007\/3-540-58179-0_69"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"A. Valmari. On-the-fly verification with stubborn sets. In CAV '93, pages 397\u2013408. Lecture Notes in Computer Science, 697, Springer Verlag, 1993.","DOI":"10.1007\/3-540-56922-7_33"}],"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\/BFb0035380","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T11:56:22Z","timestamp":1736250982000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0035380"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540627906","9783540685197"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/bfb0035380","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1997]]}}}