{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:12:46Z","timestamp":1725549166578},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642120282"},{"type":"electronic","value":"9783642120299"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-12029-9_18","type":"book-chapter","created":{"date-parts":[[2010,3,7]],"date-time":"2010-03-07T19:56:48Z","timestamp":1267991808000},"page":"248-262","source":"Crossref","is-referenced-by-count":13,"title":["An Automata-Theoretic Approach to 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"}]},{"given":"Con","family":"McGarvey","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"18_CR1","volume-title":"Model checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model checking. MIT Press, Cambridge (1999)"},{"issue":"3","key":"18_CR2","first-page":"251","volume":"21","author":"R.P. Kurshan","year":"2002","unstructured":"Kurshan, R.P., Levin, V., Minea, M., Peled, D., Yenig\u00fcn, H.: Combining software and hardware verification techniques. FMSD\u00a021(3), 251\u2013280 (2002)","journal-title":"FMSD"},{"issue":"5","key":"18_CR3","first-page":"643","volume":"80","author":"F. Xie","year":"2007","unstructured":"Xie, F., Yang, G., Song, X.: Component-based hardware\/software co-verification for building trustworthy embedded systems. JSS\u00a080(5), 643\u2013654 (2007)","journal-title":"JSS"},{"key":"18_CR4","doi-asserted-by":"crossref","unstructured":"Monniaux, D.: Verification of device drivers and intelligent controllers: a case study. In: Proc. of EMSOFT, pp. 30\u201336 (2007)","DOI":"10.1145\/1289927.1289937"},{"issue":"2","key":"18_CR5","doi-asserted-by":"publisher","first-page":"416","DOI":"10.1145\/349214.349241","volume":"22","author":"G. Ramalingam","year":"2000","unstructured":"Ramalingam, G.: Context-sensitive synchronization-sensitive analysis is undecidable. ACM Trans. Program. Lang. Syst.\u00a022(2), 416\u2013430 (2000)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"18_CR6","unstructured":"Schwoon, S.: Model-Checking Pushdown Systems. PhD thesis (2002)"},{"key":"18_CR7","volume-title":"Inside Windows NT","author":"D.A. Solomon","year":"1998","unstructured":"Solomon, D.A.: Inside Windows NT, 2nd edn. Microsoft Press, Redmond (1998)","edition":"2"},{"key":"18_CR8","unstructured":"IEEE: IEEE Standard for Verilog (IEEE Std 1364-2005). IEEE (2005)"},{"key":"18_CR9","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)"},{"issue":"2","key":"18_CR10","first-page":"366","volume":"27","author":"H. Jain","year":"2008","unstructured":"Jain, H., Kroening, D., Sharygina, N., Clarke, E.M.: Word-level predicate-abstraction and refinement techniques for verifying RTL Verilog. IEEE TCAD\u00a027(2), 366\u2013379 (2008)","journal-title":"IEEE TCAD"},{"key":"18_CR11","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, pp. 73\u201385 (2006)","DOI":"10.1145\/1217935.1217943"},{"key":"18_CR12","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: Bebop: A symbolic model checker for boolean programs. In: Proc. of SPIN, pp. 113\u2013130 (2000)","DOI":"10.1007\/10722468_7"}],"container-title":["Lecture Notes in Computer Science","Fundamental Approaches to Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-12029-9_18.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,23]],"date-time":"2020-11-23T21:46:52Z","timestamp":1606168012000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-12029-9_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642120282","9783642120299"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-12029-9_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}