{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T05:42:06Z","timestamp":1743054126470,"version":"3.40.3"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319101804"},{"type":"electronic","value":"9783319101811"}],"license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"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":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-10181-1_19","type":"book-chapter","created":{"date-parts":[[2014,8,29]],"date-time":"2014-08-29T14:28:38Z","timestamp":1409322518000},"page":"307-322","source":"Crossref","is-referenced-by-count":2,"title":["Integrating Software and Hardware Verification"],"prefix":"10.1007","author":[{"given":"Marie-Christine","family":"Jakobs","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marco","family":"Platzner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tobias","family":"Wiersema","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"19_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/978-3-642-54862-8_25","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D. Beyer","year":"2014","unstructured":"Beyer, D.: Status report on software verification. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol.\u00a08413, pp. 373\u2013388. Springer, Heidelberg (2014)"},{"key":"19_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1007\/978-3-540-73368-3_51","volume-title":"Computer Aided Verification","author":"D. Beyer","year":"2007","unstructured":"Beyer, D., Henzinger, T., Th\u00e9oduloz, G.: Configurable software verification: Concretizing the convergence of model checking and program analysis. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 504\u2013518. Springer, Heidelberg (2007)"},{"key":"19_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-642-22110-1_16","volume-title":"Computer Aided Verification","author":"D. Beyer","year":"2011","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: A Tool for Configurable Software Verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 184\u2013190. Springer, Heidelberg (2011)"},{"issue":"2-4","key":"19_CR4","first-page":"75","volume":"4","author":"A. Biere","year":"2008","unstructured":"Biere, A.: PicoSAT essentials. JSAT\u00a04(2-4), 75\u201397 (2008)","journal-title":"JSAT"},{"key":"19_CR5","doi-asserted-by":"crossref","unstructured":"Clark, N., Blome, J., Chu, M., Mahlke, S., Biles, S., Flautner, K.: An architecture framework for transparent instruction set customization in embedded processors. In: ISCA, pp. 272\u2013283. IEEE Computer Society (2005)","DOI":"10.1145\/1080695.1069993"},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"Clarke, E., Kroening, D.: Hardware verification using ANSI-C programs as a reference. In: ASP-DAC, pp. 308\u2013311. ACM (2003)","DOI":"10.1145\/1119772.1119831"},{"key":"19_CR7","doi-asserted-by":"crossref","unstructured":"Drzevitzky, S., Kastens, U., Platzner, M.: Proof-carrying hardware: Towards runtime verification of reconfigurable modules. In: ReConFig, pp. 189\u2013194. IEEE (2009)","DOI":"10.1109\/ReConFig.2009.31"},{"key":"19_CR8","doi-asserted-by":"crossref","unstructured":"Erkok, L., Carlsson, M., Wick, A.: Hardware\/software co-verification of cryptographic algorithms using Cryptol. In: FMCAD, pp. 188\u2013191. IEEE (2009)","DOI":"10.1109\/FMCAD.2009.5351121"},{"key":"19_CR9","doi-asserted-by":"crossref","unstructured":"Galuzzi, C., Bertels, K.: The instruction-set extension problem: A survey. ACM Trans. Reconfigurable Technol. Syst.\u00a04(2), 18:1\u201318:28 (2011)","DOI":"10.1145\/1968502.1968509"},{"key":"19_CR10","doi-asserted-by":"crossref","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: POPL, pp. 58\u201370. ACM (2002)","DOI":"10.1145\/565816.503279"},{"key":"19_CR11","doi-asserted-by":"crossref","unstructured":"Horn, A., Tautschnig, M., Val, C., Liang, L., Melham, T., Grundy, J., Kroening, D.: Formal co-validation of low-level hardware\/software interfaces. In: FMCAD, pp. 121\u2013128. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679400"},{"key":"19_CR12","doi-asserted-by":"crossref","unstructured":"Kurshan, R., Levin, V., Minea, M., Peled, D., Yenigun, H.: Verifying hardware in its software context. In: CAD, pp. 742\u2013749. IEEE (1997)","DOI":"10.1109\/ICCAD.1997.643621"},{"key":"19_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/978-3-642-12029-9_18","volume-title":"Fundamental Approaches to Software Engineering","author":"J. Li","year":"2010","unstructured":"Li, J., Xie, F., Ball, T., Levin, V., McGarvey, C.: An Automata-Theoretic Approach to Hardware\/Software Co-verification. In: Rosenblum, D.S., Taentzer, G. (eds.) FASE 2010. LNCS, vol.\u00a06013, pp. 248\u2013262. Springer, Heidelberg (2010)"},{"key":"19_CR14","doi-asserted-by":"crossref","unstructured":"Loitz, S., Wedler, M., Brehm, C., Vogt, T., Wehn, N., Kunz, W.: Proving functional correctness of weakly programmable IPs - a case study with formal property checking. In: SASP, pp. 48\u201354. IEEE (2008)","DOI":"10.1109\/SASP.2008.4570785"},{"key":"19_CR15","doi-asserted-by":"crossref","unstructured":"Mishchenko, A., Chatterjee, S., Brayton, R.K., E\u00e9n, N.: Improvements to combinational equivalence checking. In: ICCAD, pp. 836\u2013843. ACM (2006)","DOI":"10.1109\/ICCAD.2006.320087"},{"issue":"9","key":"19_CR16","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1145\/1995376.1995394","volume":"54","author":"L.M. de Moura","year":"2011","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM\u00a054(9), 69\u201377 (2011)","journal-title":"Commun. ACM"},{"key":"19_CR17","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Proof-carrying code. In: POPL, pp. 106\u2013119. ACM (1997)","DOI":"10.1145\/263699.263712"},{"key":"19_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-45937-5_16","volume-title":"Compiler Construction","author":"G. Necula","year":"2002","unstructured":"Necula, G., McPeak, S., Rahul, S., Weimer, W.: CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs. In: Nigel Horspool, R. (ed.) CC 2002. LNCS, vol.\u00a02304, pp. 213\u2013228. Springer, Heidelberg (2002)"},{"key":"19_CR19","doi-asserted-by":"crossref","unstructured":"Nguyen, M., Wedler, M., Stoffel, D., Kunz, W.: Formal hardware\/software co-verification by interval property checking with abstraction. In: DAC, pp. 510\u2013515. ACM (2011)","DOI":"10.1145\/2024724.2024843"},{"key":"19_CR20","doi-asserted-by":"crossref","unstructured":"Rose, J., Luu, J., Yu, C.W., Densmore, O., Goeders, J., Somerville, A., Kent, K.B., Jamieson, P., Anderson, J.: The VTR project: Architecture and CAD for FPGAs from Verilog to Routing. In: FPGA, pp. 77\u201386. ACM (2012)","DOI":"10.1145\/2145694.2145708"},{"key":"19_CR21","unstructured":"Sankaranarayanan, S., Ivancic, F.: Necla static analysis benchmarks (necla-static-small) v1.1, \n                        http:\/\/www.nec-labs.com\/research\/system\/systems_SAV-website\/small_static_bench-v1.1.tar.gz"},{"key":"19_CR22","doi-asserted-by":"crossref","unstructured":"Wagner, I., Bertacco, V.: Post-Silicon and Runtime Verification for Modern Processors. Springer (2011)","DOI":"10.1007\/978-1-4419-8034-2"},{"issue":"5","key":"19_CR23","doi-asserted-by":"publisher","first-page":"643","DOI":"10.1016\/j.jss.2006.08.015","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. Journal of Systems and Software\u00a080(5), 643\u2013654 (2007)","journal-title":"Journal of Systems and Software"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10181-1_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,28]],"date-time":"2023-01-28T08:27:06Z","timestamp":1674894426000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-10181-1_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319101804","9783319101811"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10181-1_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}