{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T13:32:09Z","timestamp":1754487129593},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540600459"},{"type":"electronic","value":"9783540494133"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60045-0_50","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:36:15Z","timestamp":1330277775000},"page":"180-195","source":"Crossref","is-referenced-by-count":24,"title":["Trace theoretic verification of asynchronous circuits using unfoldings"],"prefix":"10.1007","author":[{"given":"K. L.","family":"McMillan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"unstructured":"J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and J. Hwang. Symbolic model checking: 1020 states and beyond. In Fifth LICS, June 1990.","key":"16_CR1"},{"doi-asserted-by":"crossref","unstructured":"D. Dill. Trace theory for automatic hierarchical verification of speed-independent circuits. Technical Report 88-119, CMU, Comp. Sci. Dept., 1988.","key":"16_CR2","DOI":"10.7551\/mitpress\/6874.001.0001"},{"doi-asserted-by":"crossref","unstructured":"J. Esparza. Model checking using net unfoldings. In TAPSOFT '93, Orsay, France, April 1993.","key":"16_CR3","DOI":"10.1007\/3-540-56610-4_93"},{"doi-asserted-by":"crossref","unstructured":"P. Godefroid. Using partial orders to improve automatic verification methods. In Workshop on Computer Aided Verification, 1990.","key":"16_CR4","DOI":"10.1090\/dimacs\/003\/21"},{"doi-asserted-by":"crossref","unstructured":"P. Godefroid and P. Wolper. A partial approach to model checking. In LICS, 1991.","key":"16_CR5","DOI":"10.1109\/LICS.1991.151664"},{"unstructured":"A. J. Martin. The design of a self-timed circuit for distributed mutual exclusion. In 1985 Chapel Hill Conf. on VLSI, pages 245\u2013260, 1985.","key":"16_CR6"},{"unstructured":"K. L. McMillan. Symbolic model checking: an approach to the state explosion problem. Technical Report 92-131, CMU, Comp. Sci. Dept., 1992.","key":"16_CR7"},{"doi-asserted-by":"crossref","unstructured":"K. L. McMillan. Using unfoldings to avoid the state explosion problem in the verification of asynchronous circuits. In Fourth CAV, 1992.","key":"16_CR8","DOI":"10.1007\/3-540-56496-9_14"},{"doi-asserted-by":"crossref","unstructured":"K. L. McMillan. Symbolic Model Checking. Kluwer, 1993.","key":"16_CR9","DOI":"10.1007\/978-1-4615-3190-6"},{"doi-asserted-by":"crossref","unstructured":"K. L. McMillan. Hierarchical representations of discrete functions, with application to model checking. In Sixth CAV, Stanford, CA, 1994.","key":"16_CR10","DOI":"10.1007\/3-540-58179-0_42"},{"unstructured":"K. L. McMillan. Using unfolding to avoid the state explosion problem in the verification of asynchronous circuits. Formal Methods in System Design, 1995. to appear.","key":"16_CR11"},{"key":"16_CR12","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1016\/0304-3975(81)90112-2","volume":"13","author":"M. Nielsen","year":"1981","unstructured":"M. Nielsen, G. Plotkin, and G. Winskel. Petri nets, event structures and domains, part I. Theoretical Computer Science, 13:85\u2013108, 1981.","journal-title":"Theoretical Computer Science"},{"issue":"3","key":"16_CR13","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1145\/356698.356702","volume":"9","author":"J. L. Peterson","year":"1977","unstructured":"J. L. Peterson. Petri nets. Computing Surveys, 9(3):223\u2013248, 1977.","journal-title":"Computing Surveys"},{"doi-asserted-by":"crossref","unstructured":"D. K. Probst and H. F. Li. Using partial order semantics to avoid the state explosion problem in asynchronous systems. In CAV, 1990.","key":"16_CR14","DOI":"10.1090\/dimacs\/003\/03"},{"unstructured":"D. K. Probst and H. F. Li. Partial order model checking: A guide for the perplexed. In Third CAV, pages 405\u2013416, July 1991.","key":"16_CR15"},{"unstructured":"C. L. Seitz. System timing. In Carver Mead and Lynn Conway, editors, Introduction to VLSI Systems, pages 218\u2013262. Addison-Wesley, 1980.","key":"16_CR16"},{"unstructured":"A. Valmari. Stubborn sets for reduced state space generation. In 10th Int. Conf. on Application and Theory of Petri Nets, 1989.","key":"16_CR17"},{"doi-asserted-by":"crossref","unstructured":"A. Valmari. A stubborn attack on the state explosion problem. In Workshop on Computer Aided Verification, 1990.","key":"16_CR18","DOI":"10.1090\/dimacs\/003\/04"},{"issue":"12","key":"16_CR19","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1002\/scj.4690221204","volume":"22","author":"T. Yoneda","year":"1991","unstructured":"Tomohiro Yoneda, Yoshihiro Tohma, and Yutaka Kondo. Acceleration of timing verification method based on time Petri nets. Systems and Computers in Japan, 22(12):37\u201352, 1991.","journal-title":"Systems and Computers in Japan"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60045-0_50.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:28:53Z","timestamp":1605648533000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60045-0_50"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540600459","9783540494133"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-60045-0_50","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}