{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,1]],"date-time":"2025-06-01T04:13:06Z","timestamp":1748751186608,"version":"3.41.0"},"publisher-location":"Cham","reference-count":13,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319273396"},{"type":"electronic","value":"9783319273402"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-27340-2_75","type":"book-chapter","created":{"date-parts":[[2015,12,16]],"date-time":"2015-12-16T18:40:44Z","timestamp":1450291244000},"page":"605-614","source":"Crossref","is-referenced-by-count":1,"title":["Microprocessor Hazard Analysis Via Formal Verification of Parameterized Systems"],"prefix":"10.1007","author":[{"given":"Luk\u00e1\u0161","family":"Charv\u00e1t","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ale\u0161","family":"Smr\u010dka","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tom\u00e1\u0161","family":"Vojnar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,12,17]]},"reference":[{"key":"75_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1007\/978-3-540-39724-3_8","volume-title":"Correct Hardware Design and Verification Methods","author":"MD Aagaard","year":"2003","unstructured":"Aagaard, M.D.: A hazards-based correctness statement for pipelined circuits. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 66\u201380. Springer, Heidelberg (2003)"},{"key":"75_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1007\/978-3-642-35873-9_28","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"PA Abdulla","year":"2013","unstructured":"Abdulla, P.A., Haziza, F., Hol\u00edk, L.: All for the price of few. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 476\u2013495. Springer, Heidelberg (2013)"},{"key":"75_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/3-540-58179-0_44","volume-title":"Computer Aided Verification","author":"JR Burch","year":"1994","unstructured":"Burch, J.R., Dill, D.L.: Automatic verification of pipelined microprocessor control. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 68\u201380. Springer, Heidelberg (1994)"},{"key":"75_CR4","doi-asserted-by":"crossref","unstructured":"Charvat, L., Smrcka, A., Vojnar, T.: Automatic formal correspondence checking of ISA and RTL microprocessor description. In: Proceedings of MTV 2012, pp. 6\u201312. IEEE (2012)","DOI":"10.1109\/MTV.2012.19"},{"key":"75_CR5","doi-asserted-by":"crossref","unstructured":"Charvat, L., Smrcka, A., Vojnar, T.: Using formal verification of parameterized systems in RAW hazard analysis in microprocessors. In: Proceedings of MTV 2014, pp. 83\u201389. IEEE (2014)","DOI":"10.1109\/MTV.2014.21"},{"key":"75_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/11609773_9","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"E Clarke","year":"2006","unstructured":"Clarke, E., Talupur, M., Veith, H.: Environment abstraction for parameterized verification. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 126\u2013141. Springer, Heidelberg (2006)"},{"key":"75_CR7","doi-asserted-by":"crossref","unstructured":"Hao, K., Ray, S., Xie, F.: Equivalence checking for function pipelining in behavioral synthesis. In: Proceedings of DATE 2014, pp. 1\u20136. IEEE (2014)","DOI":"10.7873\/DATE.2014.163"},{"key":"75_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"159","DOI":"10.1007\/BFb0031806","volume-title":"Formal Methods in Computer-Aided Design","author":"RB Jones","year":"1996","unstructured":"Jones, R.B., Seger, C.H., Dill, D.L.: Self-consistency checking. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 159\u2013171. Springer, Heidelberg (1996)"},{"key":"75_CR9","doi-asserted-by":"crossref","unstructured":"Koelbl, A., Jacoby, R., Jain, H., Pixley, C.: Solver technology for system-level to RTL equivalence checking. In: Proceedings of DATE 2009, pp. 196\u2013201. IEEE (2009)","DOI":"10.1109\/DATE.2009.5090657"},{"key":"75_CR10","unstructured":"Kuhne, U., Beyer, S., Bormann, J., Barstow, J.: Automated formal verification of processors based on architectural models. In: Proceedings of FMCAD 2010, pp. 129\u2013136. IEEE (2010)"},{"key":"75_CR11","doi-asserted-by":"crossref","unstructured":"Mishra, P., Tomiyama, H., Dutt, N., Nicolau, A.: Automatic verification of in-order execution in microprocessors with fragmented pipelines and multicycle functional units. In: Proceedings of DATE 2002, pp. 36\u201343. IEEE (2002)","DOI":"10.1109\/DATE.2002.998247"},{"key":"75_CR12","volume-title":"Computer Organization and Design: The Hardware\/Software Interface","author":"DA Patterson","year":"2012","unstructured":"Patterson, D.A., Hennessy, J.L.: Computer Organization and Design: The Hardware\/Software Interface, 4th edn. Morgan Kaufmann, Boston (2012)","edition":"4"},{"key":"75_CR13","doi-asserted-by":"crossref","unstructured":"Velev, M.N., Gao, P.: Automatic formal verification of multithreaded pipelined microprocessors. In: Proceedings of ICCAD 2011, pp. 679\u2013686. IEEE (2011)","DOI":"10.1109\/ICCAD.2011.6105403"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Systems Theory \u2013 EUROCAST 2015"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-27340-2_75","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,31]],"date-time":"2025-05-31T20:26:41Z","timestamp":1748723201000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-27340-2_75"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319273396","9783319273402"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-27340-2_75","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015]]}}}