{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,24]],"date-time":"2025-08-24T01:57:30Z","timestamp":1756000650278},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540272311"},{"type":"electronic","value":"9783540316862"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11513988_20","type":"book-chapter","created":{"date-parts":[[2010,3,12]],"date-time":"2010-03-12T13:33:28Z","timestamp":1268400808000},"page":"185-198","source":"Crossref","is-referenced-by-count":28,"title":["Formal Verification of Backward Compatibility of Microcode"],"prefix":"10.1007","author":[{"given":"Tamarah","family":"Arons","sequence":"first","affiliation":[]},{"given":"Elad","family":"Elster","sequence":"additional","affiliation":[]},{"given":"Limor","family":"Fix","sequence":"additional","affiliation":[]},{"given":"Sela","family":"Mador-Haim","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Mishaeli","sequence":"additional","affiliation":[]},{"given":"Jonathan","family":"Shalev","sequence":"additional","affiliation":[]},{"given":"Eli","family":"Singerman","sequence":"additional","affiliation":[]},{"given":"Andreas","family":"Tiemeyer","sequence":"additional","affiliation":[]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[]},{"given":"Lenore D.","family":"Zuck","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"20_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/BFb0055622","volume-title":"CONCUR \u201998 Concurrency Theory","author":"R. Alur","year":"1998","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O., Vardi, M.Y.: Alternating refinement relations. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol.\u00a01466, pp. 163\u2013178. Springer, Heidelberg (1998)"},{"key":"20_CR2","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: The SLAM project: debugging system software via static analysis. In: POPL 2002, pp. 1\u20133 (2002)","DOI":"10.1145\/503272.503274"},{"key":"20_CR3","doi-asserted-by":"crossref","unstructured":"Currie, D.W., Hu, A.J., Rajan, S., Fujita, M.: Automatic formal verification of DSP software. In: DAC 2000, pp. 130\u2013135 (2000)","DOI":"10.1145\/337292.337339"},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Kroening, D., Yorav, K.: Behavioral consistency of C and Verilog programs using bounded model checking. In: DAC 2003, pp. 368\u2013371 (2003)","DOI":"10.21236\/ADA461052"},{"key":"20_CR5","unstructured":"Cyrluk, D.: Microprocessor Verification in PVS: A Methodology and Simple Example. Technical Report SRI-CSL-93-12, Menlo Park, CA (1993)"},{"key":"20_CR6","doi-asserted-by":"crossref","unstructured":"Feng, X., Hu, A.J.: Automatic formal verification for scheduled VLIW code. In: ACM SIGPLAN Joint Conference: Languages, Compilers, and Tools for Embedded Systems, and Software and Compilers for Embedded Systems, pp. 85\u201392 (2002)","DOI":"10.1145\/513829.513844"},{"key":"20_CR7","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-5693-0","volume-title":"Formal Equivalence Checking and Design Debugging","author":"S.Y. Huang","year":"1998","unstructured":"Huang, S.Y., Cheng, K.T.: Formal Equivalence Checking and Design Debugging. Kluwer, Dordrecht (1998)"},{"key":"20_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/3-540-44829-2_17","volume-title":"Model Checking Software","author":"T.A. Henzinger","year":"2003","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software verification with Blast. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 235\u2013239. Springer, Heidelberg (2003)"},{"key":"20_CR9","doi-asserted-by":"crossref","unstructured":"Harel, D., Pnueli, A.: On the development of reactive systems. In: Logics and Models of Concurrent Systems. NATO ASI Series, vol.\u00a0F-13, pp. 477\u2013498 (1985)","DOI":"10.1007\/978-3-642-82453-1_17"},{"key":"20_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1007\/3-540-40922-X_28","volume-title":"Formal Methods in Computer-Aided Design","author":"K. Hamaguchi","year":"2000","unstructured":"Hamaguchi, K., Urushihara, H., Kashiwabara, T.: Symbolic checking of signal-transition consistency for verifying high-level designs. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 455\u2013469. Springer, Heidelberg (2000)"},{"key":"20_CR11","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems: Safety","author":"Z. Manna","year":"1995","unstructured":"Manna, Z., Pnueli, A.: Temporal Verification of Reactive Systems: Safety. Springer, New York (1995)"},{"key":"20_CR12","doi-asserted-by":"crossref","unstructured":"Necula, G.: Translation validation of an optimizing compiler. In: PLDI 2000, pp. 83\u201394 (2000)","DOI":"10.1145\/349299.349314"},{"key":"20_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/BFb0054170","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Pnueli","year":"1998","unstructured":"Pnueli, A., Siegel, M., Singerman, E.: Translation validation. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol.\u00a01384, p. 151. Springer, Heidelberg (1998)"},{"issue":"2","key":"20_CR14","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1023\/A:1014122630277","volume":"20","author":"J. Sawada","year":"2002","unstructured":"Sawada, J., Hunt, W.A.: Verification of FM9801: An out-of-order microprocessor model with speculative execution, exceptions, and program-modifying capability. J. on Formal Methods in System Design\u00a020(2), 187\u2013222 (2002)","journal-title":"J. on Formal Methods in System Design"},{"key":"20_CR15","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/BF00122419","volume":"8","author":"M. Srivas","year":"1996","unstructured":"Srivas, M., Miller, S.: Applying formal verification to the AAMP5 microprocessor: A case study in the industrial use of formal methods. J. on Formal Methods in System Design\u00a08, 153\u2013188 (1996)","journal-title":"J. on Formal Methods in System Design"},{"key":"20_CR16","volume-title":"Computer Organization and Architecture","author":"W. Stallings","year":"2002","unstructured":"Stallings, W.: Computer Organization and Architecture, 6th edn. Prentice-Hall, Englewood Cliffs (2002)","edition":"6"},{"key":"20_CR17","doi-asserted-by":"crossref","unstructured":"Zuck, L., Pnueli, A., Fang, Y., Goldberg, B.: Voc: A translation validator for optimizing compilers. J. of Universal Computer Science\u00a09(2) (2003)","DOI":"10.1016\/S1571-0661(04)80393-1"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11513988_20.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,30]],"date-time":"2023-05-30T23:47:33Z","timestamp":1685490453000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11513988_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540272311","9783540316862"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/11513988_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}