{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:56:10Z","timestamp":1725558970976},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642142949"},{"type":"electronic","value":"9783642142956"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14295-6_30","type":"book-chapter","created":{"date-parts":[[2010,7,8]],"date-time":"2010-07-08T22:36:09Z","timestamp":1278628569000},"page":"339-353","source":"Crossref","is-referenced-by-count":1,"title":["Efficient Reachability Analysis of B\u00fcchi Pushdown Systems for Hardware\/Software Co-verification"],"prefix":"10.1007","author":[{"given":"Juncao","family":"Li","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fei","family":"Xie","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thomas","family":"Ball","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vladimir","family":"Levin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"30_CR1","doi-asserted-by":"crossref","unstructured":"Li, J., Xie, F., Ball, T., Levin, V., McGarvey, C.: An automata-theoretic approach to hardware\/software co-verification. In: Proc. of FASE (2010)","DOI":"10.1007\/978-3-642-12029-9_18"},{"key":"30_CR2","unstructured":"Schwoon, S.: Model-Checking Pushdown Systems. PhD thesis (2002)"},{"key":"30_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/BFb0054182","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R.P. Kurshan","year":"1998","unstructured":"Kurshan, R.P., Levin, V., Minea, M., Peled, D., Yenig\u00fcn, H.: Static partial order reduction. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, p. 345. Springer, Heidelberg (1998)"},{"key":"30_CR4","doi-asserted-by":"crossref","unstructured":"Ball, T., Bounimova, E., Cook, B., Levin, V., Lichtenberg, J., McGarvey, C., Ondrusek, B., Rajamani, S.K., Ustuner, A.: Thorough static analysis of device drivers. In: Proc. of EuroSys (2006)","DOI":"10.1145\/1217935.1217943"},{"key":"30_CR5","unstructured":"Kurshan, R.P., Levin, V., Minea, M., Peled, D., Yenig\u00fcn, H.: Combining software and hardware verification techniques. FMSD (2002)"},{"key":"30_CR6","doi-asserted-by":"crossref","unstructured":"Xie, F., Yang, G., Song, X.: Component-based hardware\/software co-verification for building trustworthy embedded systems. JSS\u00a080(5) (2007)","DOI":"10.1016\/j.jss.2006.08.015"},{"key":"30_CR7","doi-asserted-by":"crossref","unstructured":"Monniaux, D.: Verification of device drivers and intelligent controllers: a case study. In: Proc. of EMSOFT (2007)","DOI":"10.1145\/1289927.1289937"},{"key":"30_CR8","doi-asserted-by":"crossref","unstructured":"Ramalingam, G.: Context-sensitive synchronization-sensitive analysis is undecidable. ACM Trans. Program. Lang. Syst. (2000)","DOI":"10.1145\/349214.349241"},{"key":"30_CR9","series-title":"Lecture Notes in Computer Science","volume-title":"CONCUR\u201997: Concurrency Theory","author":"A. Bouajjani","year":"1997","unstructured":"A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model-checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol.\u00a01243, Springer, Heidelberg (1997)"},{"key":"30_CR10","unstructured":"Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem. PhD thesis (1994)"},{"key":"30_CR11","volume-title":"Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach","author":"R.P. Kurshan","year":"1994","unstructured":"Kurshan, R.P.: Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton University Press, Princeton (1994)"},{"key":"30_CR12","unstructured":"Microsoft: Synchronizing interrupt code. In: MSDN (2009), \n                    \n                      msdn.microsoft.com\/en-us\/library\/aa490313.aspx"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14295-6_30","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T19:51:03Z","timestamp":1558295463000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14295-6_30"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642142949","9783642142956"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14295-6_30","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}