{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T21:03:06Z","timestamp":1744232586202},"publisher-location":"Cham","reference-count":13,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319107011"},{"type":"electronic","value":"9783319107028"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-10702-8_13","type":"book-chapter","created":{"date-parts":[[2014,9,1]],"date-time":"2014-09-01T08:19:16Z","timestamp":1409559556000},"page":"185-199","source":"Crossref","is-referenced-by-count":14,"title":["Randomised Testing of a Microprocessor Model Using SMT-Solver State Generation"],"prefix":"10.1007","author":[{"given":"Brian","family":"Campbell","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ian","family":"Stark","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"13_CR1","unstructured":"ARM: ARMv6-M Architecture Reference Manual, document DDI 0419C (2010), \n                  \n                    http:\/\/infocenter.arm.com\/help\/topic\/com.arm.doc.ddi0419c\/index.html"},{"issue":"4-5","key":"13_CR2","doi-asserted-by":"publisher","first-page":"411","DOI":"10.1007\/s10009-006-0204-6","volume":"8","author":"S. Beyer","year":"2006","unstructured":"Beyer, S., Jacobi, C., Kr\u00f6ning, D., Leinenbach, D., Paul, W.J.: Putting it all together \u2014 formal verification of the VAMP. International Journal on Software Tools for Technology Transfer\u00a08(4-5), 411\u2013430 (2006)","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"Bounimova, E., Godefroid, P., Molnar, D.: Billions and billions of constraints: Whitebox fuzz testing in production. In: Proceedings of the 2013 International Conference on Software Engineering, ICSE 2013, pp. 122\u2013131. IEEE (2013)","DOI":"10.1109\/ICSE.2013.6606558"},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/978-3-642-38916-0_5","volume-title":"Tests and Proofs","author":"A.D. Brucker","year":"2013","unstructured":"Brucker, A.D., Feliachi, A., Nemouchi, Y., Wolff, B.: Test program generation for a microprocessor. In: Veanes, M., Vigan\u00f2, L. (eds.) TAP 2013. LNCS, vol.\u00a07942, pp. 76\u201395. Springer, Heidelberg (2013)"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/10930755_2","volume-title":"Theorem Proving in Higher Order Logics","author":"A. Fox","year":"2003","unstructured":"Fox, A.: Formal specification and verification of ARM6. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol.\u00a02758, pp. 25\u201340. Springer, Heidelberg (2003)"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1007\/978-3-642-32347-8_23","volume-title":"Interactive Theorem Proving","author":"A. Fox","year":"2012","unstructured":"Fox, A.: Directions in ISA specification. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol.\u00a07406, pp. 338\u2013344. Springer, Heidelberg (2012)"},{"key":"13_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-642-14052-5_18","volume-title":"Interactive Theorem Proving","author":"A. Fox","year":"2010","unstructured":"Fox, A., Myreen, M.O.: A trustworthy monadic formalization of the ARMv7 instruction set architecture. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol.\u00a06172, pp. 243\u2013258. Springer, Heidelberg (2010)"},{"key":"13_CR8","unstructured":"HOL4, \n                  \n                    http:\/\/hol.sourceforge.net\/"},{"key":"13_CR9","unstructured":"Myreen, M.O., Gordon, M.J.C., Slind, K.: Decompilation into logic - improved. In: Cabodi, G., Singh, S. (eds.) FMCAD, pp. 78\u201381. IEEE (2012)"},{"key":"13_CR10","unstructured":"Open on-chip debugger (2014), \n                  \n                    http:\/\/openocd.sourceforge.net\/"},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/3-540-49519-3_22","volume-title":"Formal Methods in Computer-Aided Design","author":"J. Strother Moore","year":"1998","unstructured":"Strother Moore, J.: Symbolic simulation: An ACL2 approach. In: Gopalakrishnan, G., Windley, P. (eds.) FMCAD 1998. LNCS, vol.\u00a01522, pp. 334\u2013350. Springer, Heidelberg (1998)"},{"issue":"5","key":"13_CR12","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/s10009-011-0188-8","volume":"13","author":"T. Weber","year":"2011","unstructured":"Weber, T.: SMT solvers: New oracles for the HOL theorem prover. International Journal on Software Tools for Technology Transfer (STTT)\u00a013(5), 419\u2013429 (2011)","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"Wilhelm, R., Engblom, J., Ermedahl, A., Holsti, N., Thesing, S., Whalley, D., Bernat, G., Ferdinand, C., Heckmann, R., Mitra, T., Mueller, F., Puaut, I., Puschner, P., Staschulat, J., Stenstr\u00f6m, P.: The worst-case execution-time problem\u2014overview of methods and survey of tools. ACM Trans. Embed. Comput. Syst.\u00a07, 36:1\u201336:53 (2008)","DOI":"10.1145\/1347375.1347389"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10702-8_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T15:01:58Z","timestamp":1558969318000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10702-8_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319107011","9783319107028"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10702-8_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}