{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,7]],"date-time":"2026-05-07T02:45:02Z","timestamp":1778121902768,"version":"3.51.4"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319415390","type":"print"},{"value":"9783319415406","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-41540-6_3","type":"book-chapter","created":{"date-parts":[[2016,7,12]],"date-time":"2016-07-12T09:34:07Z","timestamp":1468316047000},"page":"42-58","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":39,"title":["End-to-End Verification of \"Equation missing\" Processors with ISA-Formal"],"prefix":"10.1007","author":[{"given":"Alastair","family":"Reid","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rick","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anastasios","family":"Deligiannis","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Gilday","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Hoyes","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Will","family":"Keen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ashan","family":"Pathirane","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Owen","family":"Shepherd","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Vrabel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ali","family":"Zaidi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,7,13]]},"reference":[{"key":"3_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/3-540-44798-9_33","volume-title":"Correct Hardware Design and Verification Methods","author":"MD Aagaard","year":"2001","unstructured":"Aagaard, M.D., Cook, B., Day, N.A., Jones, R.B.: A framework for microprocessor correctness statements. In: Margaria, T., Melham, T.F. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 433\u2013448. Springer, Heidelberg (2001). \n                      http:\/\/dl.acm.org\/citation.cfm?id=646705.702043"},{"key":"3_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/3-540-40922-X_17","volume-title":"Formal Methods in Computer-Aided Design","author":"MD Aagaard","year":"2000","unstructured":"Aagaard, M.D., Jones, R.B., Melham, T.F., O\u2019Leary, J.W., Seger, C.-J.H.: A methodology for large-scale hardware verification. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol. 1954, pp. 300\u2013319. Springer, Heidelberg (2000)"},{"key":"3_CR3","unstructured":"ARM Ltd: ARM Architecture Reference Manual (ARMv8, for ARMv8-A architecture profile). ARM Ltd (2013)"},{"key":"3_CR4","unstructured":"ARM Ltd: (In Preparation) ARM Architecture Reference Manual (ARMv8, for ARMv8-M architecture profile). ARM Ltd (2016)"},{"key":"3_CR5","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). \n                      http:\/\/dl.acm.org\/citation.cfm?id=647763.735662"},{"key":"3_CR6","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. 6172, pp. 243\u2013258. Springer, Heidelberg (2010). doi:\n                      10.1007\/978-3-642-14052-5_18"},{"key":"3_CR7","doi-asserted-by":"crossref","unstructured":"Higgins, J.T., Aagaard, M.D.: Simplifying design and verification for structural hazards and datapaths in pipelined circuits. In: Ninth IEEE International Proceedings of the High-Level Design Validation and Test Workshop, HLDVT 2004, pp. 31\u201336 (2004). \n                      http:\/\/dx.doi.org\/10.1109\/HLDVT.2004.1431229","DOI":"10.1109\/HLDVT.2004.1431229"},{"issue":"3","key":"3_CR8","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1109\/40.768503","volume":"19","author":"WA Hunt Jr","year":"1999","unstructured":"Hunt Jr., W.A., Sawada, J.: Verifying the FM9801 microarchitecture. IEEE Micro 19(3), 47\u201355 (1999). doi:\n                      10.1109\/40.768503","journal-title":"IEEE Micro"},{"key":"3_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/3-540-44585-4_40","volume-title":"Computer Aided Verification","author":"R Jhalal","year":"2001","unstructured":"Jhalal, R., McMillan, K.L.: Microarchitecture verification by compositional model checking. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 396. Springer, Heidelberg (2001). doi:\n                      10.1007\/3-540-44585-4_40"},{"key":"3_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"414","DOI":"10.1007\/978-3-642-02658-4_32","volume-title":"Computer Aided Verification","author":"R Kaivola","year":"2009","unstructured":"Kaivola, R., et al.: Replacing testing with formal verification in Intel$$^{\\textregistered }$$ Core$$^\\text{ TM }$$ i7 processor execution engine validation. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 414\u2013429. Springer, Heidelberg (2009). \n                      http:\/\/dx.doi.org\/10.1007\/978-3-642-02658-4_32"},{"key":"3_CR11","unstructured":"KiranKumar, V., Gupta, A., Ghughal, R.: Symbolic trajectory evaluation: the primary validation vehicle for next generation Intel processor graphics FPU. In: Formal Methods in Computer-Aided Design (FMCAD), pp. 149\u2013156. IEEE (2012)"},{"key":"3_CR12","unstructured":"Kroening, D., Paul, W., Mueller, S.: Proving the correctness of pipelined micro-architectures. In: Waldschmidt, K., Grimm, C. (eds.) Proceedings of ITG\/GI\/GMM-Workshop \u201cMethoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen\u201d, pp. 89\u201398. VDE Verlag (2000)"},{"key":"3_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1007\/978-3-540-45069-6_33","volume-title":"Computer Aided Verification","author":"SK Lahiri","year":"2003","unstructured":"Lahiri, S.K., Bryant, R.E.: Deductive verification of advanced out-of-order microprocessors. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 341\u2013354. Springer, Heidelberg (2003). doi:\n                      10.1007\/978-3-540-45069-6_33"},{"key":"3_CR14","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Pixley, C., Albin, K.: Experience with term level modeling and verification of the M*CORE$${}^{TM}$$ microprocessor core. In: Proceedings of the Sixth IEEE International High-Level Design Validation and Test Workshop 2001, Monterey, California, USA, 7\u20139 November 2001, pp. 109\u2013114 (2001). \n                      http:\/\/dx.doi.org\/10.1109\/HLDVT.2001.972816","DOI":"10.1109\/HLDVT.2001.972816"},{"key":"3_CR15","unstructured":"Malik, N., Eickemeyer, R.J., Vassiliadis, S.: Interlock collapsing ALU for increased instruction-level parallelism. In: Proceedings of the 25th Annual International Symposium on Microarchitecture, pp. 149\u2013157. MICRO 25, CA (1992). \n                      http:\/\/dl.acm.org\/citation.cfm?id=144953.145794"},{"key":"3_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/BFb0028738","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"1998","unstructured":"McMillan, K.L.: Verification of an implementation of Tomasulo\u2019s algorithm by compositional model checking. In: Vardi, M.Y. (ed.) CAV 1998. LNCS, vol. 1427, pp. 110\u2013121. Springer, Heidelberg (1998). \n                      http:\/\/dl.acm.org\/citation.cfm?id=647767.733764"},{"key":"3_CR17","doi-asserted-by":"crossref","unstructured":"Reid, A.: Creating trustworthy specifications of ARM v8-A and v8-M system level architecture. In: preparation (2016)","DOI":"10.1109\/FMCAD.2016.7886675"},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"Slobodov\u00e1, A., Davis, J., Swords, S., Hunt Jr., W.: A flexible formal verification framework for industrial scale validation. In: 2011 9th IEEE\/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE), pp. 89\u201397. IEEE (2011)","DOI":"10.1109\/MEMCOD.2011.5970515"},{"issue":"8","key":"3_CR19","doi-asserted-by":"publisher","first-page":"1138","DOI":"10.1109\/TC.2010.18","volume":"59","author":"SK Srinivasan","year":"2010","unstructured":"Srinivasan, S.K.: Automatic refinement checking of pipelines with out-of-order execution. IEEE Trans. Comput. 59(8), 1138\u20131144 (2010)","journal-title":"IEEE Trans. Comput."},{"key":"3_CR20","unstructured":"Stewart, D., Gilday, D., Nevill, D., Roberts, T.: Processor memory system verification using DOGReL: a language for specifying end-to-end properties. In: International Workshop on Design and Implementation of Formal Tools and Systems, DIFTS 2014 (2014)"},{"issue":"1","key":"3_CR21","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1109\/12.368009","volume":"44","author":"PJ Windley","year":"1995","unstructured":"Windley, P.J.: Formal modeling and verification of microprocessors. IEEE Trans. Comput. 44(1), 54\u201372 (1995)","journal-title":"IEEE Trans. Comput."}],"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-319-41540-6_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,7,14]],"date-time":"2020-07-14T00:07:17Z","timestamp":1594685237000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-41540-6_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319415390","9783319415406"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-41540-6_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"13 July 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Toronto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 July 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 July 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}