{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,14]],"date-time":"2025-03-14T04:07:39Z","timestamp":1741925259443,"version":"3.38.0"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642245589"},{"type":"electronic","value":"9783642245596"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-24559-6_39","type":"book-chapter","created":{"date-parts":[[2011,10,21]],"date-time":"2011-10-21T15:13:17Z","timestamp":1319209997000},"page":"585-600","source":"Crossref","is-referenced-by-count":1,"title":["Managing Complexity through Abstraction: A Refinement-Based Approach to Formalize Instruction Set Architectures"],"prefix":"10.1007","author":[{"given":"Fangfang","family":"Yuan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stephen","family":"Wright","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kerstin","family":"Eder","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"May","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"39_CR1","unstructured":"International Technology Roadmap for Semiconductors, chap. Design, p.\u00a019 (2009), http:\/\/www.itrs.net"},{"key":"39_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511624162","volume-title":"The B-book: Assigning Programs to Meanings","author":"J.R. Abrial","year":"1996","unstructured":"Abrial, J.R.: The B-book: Assigning Programs to Meanings. Cambridge University Press, New York (1996)"},{"key":"39_CR3","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139195881","volume-title":"Modeling in Event-B: System and Software Engineering","author":"J.R. Abrial","year":"2010","unstructured":"Abrial, J.R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press, Cambridge (2010)"},{"issue":"6","key":"39_CR4","doi-asserted-by":"publisher","first-page":"447","DOI":"10.1007\/s10009-010-0145-y","volume":"12","author":"J.R. Abrial","year":"2010","unstructured":"Abrial, J.R., Butler, M., Hallerstede, S., Hoang, T.S., Mehta, F., Voisin, L.: Rodin: An open toolset for modelling and reasoning in Event-B. STTT\u00a012(6), 447\u2013466 (2010)","journal-title":"STTT"},{"key":"39_CR5","unstructured":"ARM Ltd: ARM Architecture Refernce Manual, AMVv7-A and ARMv7-R edn."},{"key":"39_CR6","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/s10766-005-7301-0","volume":"33","author":"R. Azevedo","year":"2005","unstructured":"Azevedo, R., Rigo, S., Bartholomeu, M., Araujo, G., Araujo, C., Barros, E.: The ArchC architecture description language and tools. Int. J. Parallel Program.\u00a033, 453\u2013484 (2005)","journal-title":"Int. J. Parallel Program."},{"key":"39_CR7","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-0302-6","volume-title":"Writing Testbenches: Functional Verification of HDL Models","author":"J. Bergeron","year":"2003","unstructured":"Bergeron, J.: Writing Testbenches: Functional Verification of HDL Models, 2nd edn. Springer, Heidelberg (2003)","edition":"2"},{"issue":"1-5","key":"39_CR8","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1016\/0165-6074(87)90042-1","volume":"21","author":"J.P. Bowen","year":"1987","unstructured":"Bowen, J.P.: Formal specification and documentation of microprocessor instruction sets. Microprocess. Microprogram\u00a021(1-5), 223\u2013230 (1987)","journal-title":"Microprocess. Microprogram"},{"key":"39_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1352582.1352588","volume":"9","author":"H. Chockler","year":"2008","unstructured":"Chockler, H., Halpern, J.Y., Kupferman, O.: What causes a system to satisfy a specification? ACM Transactions on Computational Logic\u00a09, 1\u201326 (2008)","journal-title":"ACM Transactions on Computational Logic"},{"key":"39_CR10","unstructured":"Fox, A.: A HOL specification of the ARM instruction set architecture. Tech. Rep. UCAM-CL-TR-545, University of Cambridge, Computer Laboratory (June 2001)"},{"key":"39_CR11","unstructured":"Fox, A.: An algebraic framework for modelling and verifying microprocessors using HOL. Tech. Rep. UCAM-CL-TR-512, University of Cambridge, Computer Laboratory (March 2001)"},{"key":"39_CR12","doi-asserted-by":"crossref","unstructured":"Fox, A., Myreen, M.: A trustworthy monadic formalization of the ARMv7 instruction set architecture. Interactive Theorem Proving, ITP (2010)","DOI":"10.1007\/978-3-642-14052-5_18"},{"issue":"1","key":"39_CR13","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/s00165-009-0138-3","volume":"23","author":"S. Hallerstede","year":"2011","unstructured":"Hallerstede, S.: On the purpose of Event-B proof obligations. Formal Aspects of Computing\u00a023(1), 133\u2013150 (2011)","journal-title":"Formal Aspects of Computing"},{"key":"39_CR14","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/BFb0021717","volume-title":"Proceedings of the IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods","author":"N.A. Harman","year":"1993","unstructured":"Harman, N.A., Tucker, J.V.: Algebraic models and the correctness of microprocessors. In: Proceedings of the IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, pp. 92\u2013108. Springer, Heidelberg (1993)"},{"key":"39_CR15","volume-title":"Computer Architecture: A Quantitative Approach","author":"J.L. Hennessy","year":"2002","unstructured":"Hennessy, J.L., Patterson, D.A.: Computer Architecture: A Quantitative Approach, 3rd edn. Morgan Kaufmann, San Francisco (2002)","edition":"3"},{"issue":"4","key":"39_CR16","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1109\/54.936245","volume":"18","author":"R.B. Jones","year":"2001","unstructured":"Jones, R.B., O\u2019Leary, J.W., Seger, C.J.H., Aagaard, M.D., Melham, T.F.: Practical formal verification in microprocessor design. IEEE Design & Test of Computers\u00a018(4), 16\u201325 (2001)","journal-title":"IEEE Design & Test of Computers"},{"key":"39_CR17","doi-asserted-by":"crossref","unstructured":"May, D.: The XMOS XS1 Architecture. XMOS Limited (2009)","DOI":"10.1109\/HOTCHIPS.2011.7477496"},{"key":"39_CR18","doi-asserted-by":"crossref","unstructured":"Medeiros Jr., V., D\u00e9harbe, D.: Formal Modelling of a Microcontroller Instruction Set in B. In: Formal Methods: Foundations and Applications: 12th Brazilian Symposium on Formal Methods, pp. 282\u2013289 (2009)","DOI":"10.1007\/978-3-642-10452-7_19"},{"key":"39_CR19","unstructured":"Page, D.: CRISP: A Cryptographic RISC Processor, pagecs.bris.ac.uk"},{"key":"39_CR20","unstructured":"ProB, http:\/\/www.stups.uni-duesseldorf.de\/ProB\/"},{"key":"39_CR21","volume-title":"Comprehensive Functional Verification","author":"B. Wile","year":"2005","unstructured":"Wile, B., Goss, J.C., Roesner, W.: Comprehensive Functional Verification. Morgan Kaufmann, San Francisco (2005)"},{"key":"39_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/3-540-58450-1_59","volume-title":"Higher Order Logic Theorem Proving and Its Applications","author":"P.J. Windley","year":"1994","unstructured":"Windley, P.J.: Specifying Instruction-Set Architectures in HOL: A Primer. In: Melham, T.F., Camilleri, J. (eds.) HUG 1994. LNCS, vol.\u00a0859, pp. 440\u2013455. Springer, Heidelberg (1994)"},{"key":"39_CR23","unstructured":"Wright, S.: Automatic Generation of C from Event-B. In: IM_FMT 2009 Workshop on Integration of Model-based Formal Methods and Tools (February 2009)"},{"issue":"1","key":"39_CR24","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/s00165-009-0142-7","volume":"23","author":"S. Wright","year":"2010","unstructured":"Wright, S., Eder, K.: Using Event-B to construct instruction set architectures. Formal Aspects of Computing\u00a023(1), 73\u201389 (2010)","journal-title":"Formal Aspects of Computing"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-24559-6_39","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,13]],"date-time":"2025-03-13T04:59:37Z","timestamp":1741841977000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-24559-6_39"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642245589","9783642245596"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-24559-6_39","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}