{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T12:29:21Z","timestamp":1754396961963,"version":"3.32.0"},"reference-count":49,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2006,10,7]],"date-time":"2006-10-07T00:00:00Z","timestamp":1160179200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2007,1,17]]},"DOI":"10.1007\/s10817-006-9035-0","type":"journal-article","created":{"date-parts":[[2006,10,6]],"date-time":"2006-10-06T12:33:05Z","timestamp":1160137985000},"page":"93-116","source":"Crossref","is-referenced-by-count":11,"title":["A Framework for Verifying Bit-Level Pipelined Machines Based on Automated Deduction and Decision Procedures"],"prefix":"10.1007","volume":"37","author":[{"given":"Panagiotis","family":"Manolios","sequence":"first","affiliation":[]},{"given":"Sudarshan K.","family":"Srinivasan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2006,10,7]]},"reference":[{"key":"9035_CR1","doi-asserted-by":"crossref","unstructured":"Andraus, Z.S., Sakallah, K.A.: Automatic abstraction and verification of Verilog models. In: Malik, S., Fix, L., Kahng, A.B. (eds.) Design Automation Conference \u2013 DAC'04, pp. 218\u2013223 (2004)","DOI":"10.1145\/996566.996629"},{"key":"9035_CR2","doi-asserted-by":"crossref","unstructured":"Arons, T., Pnueli, A.: A comparison of two verification methods for speculative instruction execution. In: Tools and Algorithms for the Construction and Analysis of Systems \u2013 TACAS'00, Vol. 1785 of LNCS, pp. 487\u2013502 (2000)","DOI":"10.1007\/3-540-46419-0_33"},{"key":"9035_CR3","doi-asserted-by":"crossref","unstructured":"Bentley, B.: Validating the Intel Pentium 4 microprocessor. In: 38th Design Automation Conference \u2013 DAC'01, pp. 253\u2013255 (2001)","DOI":"10.1145\/378239.378473"},{"key":"9035_CR4","unstructured":"Bentley, B.: Validating a modern microprocessor. See URL http:\/\/www.cav2005.inf.ed.ac.uk\/bentley_CAV_07_08_2005.ppt (2005)"},{"issue":"4","key":"9035_CR5","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/BF00243131","volume":"5","author":"W.R. Bevier","year":"1989","unstructured":"Bevier, W.R., Hunt, Jr., W.A., Moore, J.S., Young, W.D.: An approach to systems verification. J. Autom. Reason. 5(4), 411\u2013428 (1989)","journal-title":"J. Autom. Reason."},{"key":"9035_CR6","unstructured":"Boyer, R.S., Moore, JS.: Integrating decision procedures into heuristic theorem provers: A case study of linear arithmetic. In: Machine Intelligence 11, pp. 83\u2013124. Oxford University Press (1988)"},{"key":"9035_CR7","doi-asserted-by":"crossref","unstructured":"Brock, B., Hunt, Jr., W.A.: Formally specifying and mechanically verifying programs for the Motorola Complex Arithmetic Processor DSP. In: 1997 IEEE International Conference on Computer Design, pp. 31\u201336 (1997)","DOI":"10.1109\/ICCD.1997.628846"},{"key":"9035_CR8","doi-asserted-by":"crossref","unstructured":"Browne, M., Clarke, E.M., Grumberg, O.: Characterizing finite Kripke structures in propositional temporal logic. Theor. Comp. Sci. 59 (1988)","DOI":"10.21236\/ADA188620"},{"key":"9035_CR9","doi-asserted-by":"crossref","unstructured":"Bryant, R.E., German, S., Velev, M.N.: Exploiting positive equality in a logic of equality with uninterpreted functions. In: Halbwachs, N., Peled, D. (eds.) Computer-Aided Verification \u2013 CAV'99, Vol. 1633 of LNCS, pp. 470\u2013482 (1999)","DOI":"10.1007\/3-540-48683-6_40"},{"key":"9035_CR10","doi-asserted-by":"crossref","unstructured":"Bryant, R.E., Lahiri, S.K., Seshia, S.: Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In: Brinksma, E., Larsen, K. (eds.) Computer-Aided Verification \u2013 CAV'02, Vol. 2404 of LNCS, pp. 78\u201392 (2002)","DOI":"10.1007\/3-540-45657-0_7"},{"key":"9035_CR11","doi-asserted-by":"crossref","unstructured":"Burch, J.R., Dill, D.L.: Automatic verification of pipelined microprocessor control. In: Computer-Aided Verification \u2013 CAV'94, Vol. 818 of LNCS, pp. 68\u201380 (1994)","DOI":"10.1007\/3-540-58179-0_44"},{"issue":"11","key":"9035_CR12","doi-asserted-by":"crossref","first-page":"1544","DOI":"10.1109\/4.962279","volume":"36","author":"L. Clark","year":"2001","unstructured":"Clark, L., Hoffman, E., Miller, J., Biyani, M., Liao, Y., Strazdus, S., Morrow, M., Velarde, K., Yarch, M.: An embedded 32-bit microprocessor core for low-power and high-performance applications. IEEE J. Solid-State Circuits 36(11), 1544\u20131608 (2001)","journal-title":"IEEE J. Solid-State Circuits"},{"key":"9035_CR13","unstructured":"de Moura, L.: Yices homepage. See URL http:\/\/fm.csl.sri.com\/yices (2005)"},{"key":"9035_CR14","doi-asserted-by":"crossref","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast decision procedures. In: Alur, R., Peled, D. (eds.) Computer Aided Verification \u2013 CAV'04, Vol. 3114 of LNCS, pp. 175\u2013188 (2004)","DOI":"10.1007\/978-3-540-27813-9_14"},{"key":"9035_CR15","unstructured":"Greve, D., Richards, R., Wilding, M.: A summary of intrinsic partitioning verification. In: Fifth International Workshop on the ACL2 Theorem Prover and Its Applications (2004)"},{"key":"9035_CR16","doi-asserted-by":"crossref","unstructured":"Greve, D., Wilding, M., Hardin, D.: High-speed, analyzable simulators. In: Kaufmann, M., Manolios, P., Moore, JS. (eds.) Computer-Aided Reasoning: ACL2 Case Studies. Kluwer, pp. 113\u2013135 (2000)","DOI":"10.1007\/978-1-4757-3188-0_8"},{"key":"9035_CR17","doi-asserted-by":"crossref","unstructured":"Hosabettu, R., Srivas, M., Gopalakrishnan, G.: Decomposing the proof of correctness of a pileplined microprocessors. In: Hu, A.J., Vardi, M.Y. (eds.): Computer-Aided Verification \u2013 CAV'98, Vol. 1427 of LNCS (1998)","DOI":"10.1007\/BFb0028739"},{"key":"9035_CR18","doi-asserted-by":"crossref","unstructured":"Hosabettu, R., Srivas, M., Gopalakrishnan, G.: Proof of correctness of a processor with reorder buffer using the completion functions approach. In: Halbwachs, N., Peled, D. (eds.) Computer-Aided Verification \u2013 CAV'99, Vol. 1633 of LNCS (1999)","DOI":"10.1007\/3-540-48683-6_7"},{"issue":"4","key":"9035_CR19","doi-asserted-by":"crossref","first-page":"429","DOI":"10.1007\/BF00243132","volume":"5","author":"W.A. Hunt Jr.","year":"1989","unstructured":"Hunt, Jr., W.A.: Microprocessor design verification. J. Autom. Reason. 5(4), 429\u2013460 (1989)","journal-title":"J. Autom. Reason."},{"key":"9035_CR20","doi-asserted-by":"crossref","unstructured":"Hunt, Jr., W.A.: FM8501: A Verified Microprocessor, Vol. 795. Springer, Berlin Heidelberg New York (1994)","DOI":"10.1007\/3-540-57960-5"},{"key":"9035_CR21","doi-asserted-by":"crossref","unstructured":"Jouannaud, J.-P. (ed.) Functional Programming Languages and Computer Architecture, No. 201. Nancy, France (1985)","DOI":"10.1007\/3-540-15975-4"},{"key":"9035_CR22","doi-asserted-by":"crossref","unstructured":"Kaufmann, M., Manolios, P., Moore, JS. (eds.): Computer-Aided Reasoning: ACL2 Case Studies. Kluwer (2000a)","DOI":"10.1007\/978-1-4615-4449-4"},{"key":"9035_CR23","doi-asserted-by":"crossref","unstructured":"Kaufmann, M., Manolios, P., Moore, JS.: Computer-Aided Reasoning: An Approach. Kluwer (2000b)","DOI":"10.1007\/978-1-4615-4449-4"},{"key":"9035_CR24","unstructured":"Kaufmann, M., Moore, JS.: ACL2 homepage. See URL http:\/\/www.cs.utexas.edu\/users\/moore\/-acl2 (2004)"},{"key":"9035_CR25","unstructured":"Kroning, D.: Formal verification of pipelined microprocessors. PhD thesis, Universit\u00e4t des Saarlandes (2001)"},{"key":"9035_CR26","doi-asserted-by":"crossref","unstructured":"Lahiri, S., Seshia, S., Bryant, R.: Modeling and verification of out-of-order microprocessors using UCLID. In: Formal Methods in Computer-Aided Design \u2013 FMCAD'02, Vol. 2517 of LNCS, pp. 142\u2013159 (2002)","DOI":"10.1007\/3-540-36126-X_9"},{"key":"9035_CR27","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Seshia, S.: The UCLID decision procedure. In: Computer Aided Verification \u2013 CAV'04, Vol. 3114 of LNCS, pp. 475\u2013478 (2004)","DOI":"10.1007\/978-3-540-27813-9_40"},{"issue":"4","key":"9035_CR28","doi-asserted-by":"crossref","first-page":"308","DOI":"10.1093\/comjnl\/6.4.308","volume":"6","author":"P.J. Landin","year":"1964","unstructured":"Landin, P.J.: The mechanical evaluation of expressions. Comput. J. 6(4), 308\u2013320 (1964)","journal-title":"Comput. J."},{"key":"9035_CR29","doi-asserted-by":"crossref","unstructured":"Manolios, P.: Correctness of pipelined machines. In: Hunt, Jr., W.A., Johnson, S.D. (eds.) Formal Methods in Computer-Aided Design \u2013 FMCAD'00, Vol. 1954 of LNCS, pp. 161\u2013178 (2000)","DOI":"10.1007\/3-540-40922-X_11"},{"key":"9035_CR30","unstructured":"Manolios, P.: Mechanical verification of reactive systems. PhD thesis, University of Texas at Austin. See URL http:\/\/www.cc.gatech.edu\/~manolios\/publications.html"},{"key":"9035_CR31","doi-asserted-by":"crossref","unstructured":"Manolios, P.: A compositional theory of refinement for branching time. In: Geist, D., Tronci, E. (eds.) 12th IFIP WG 10.5 Advanced Research Working Conference \u2013 CHARME'03, Vol. 2860 of LNCS, pp. 304\u2013318 (2003)","DOI":"10.1007\/978-3-540-39724-3_28"},{"key":"9035_CR32","doi-asserted-by":"crossref","unstructured":"Manolios, P., Srinivasan, S.: Automatic verification of safety and liveness for XScale-like processor models using WEB-refinements. In: Design Automation and Test in Europe \u2013 DATE'04, pp. 168\u2013175 (2004a)","DOI":"10.1109\/DATE.2004.1268844"},{"key":"9035_CR33","unstructured":"Manolios, P., Srinivasan, S.: A suite of hard ACL2 theorems arising in refinement-based processor verification. In: Kaufmann, M., Moore, J.S. (eds.) Fifth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2004). See URL http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/workshop-2004\/ (2004b)"},{"key":"9035_CR34","doi-asserted-by":"crossref","unstructured":"Manolios, P., Srinivasan, S.: A complete compositional reasoning framework for the efficient verification of pipelined machines. In: International Conference on Computer-Aided Design \u2013 ICCAD'05, pp. 863\u2013870 (2005a)","DOI":"10.1109\/ICCAD.2005.1560183"},{"key":"9035_CR35","doi-asserted-by":"crossref","unstructured":"Manolios, P., Srinivasan, S.: Refinement maps for efficient verification of processor models. In: Design Automation and Test in Europe \u2013 DATE'05, pp. 1304\u20131309 (2005b)","DOI":"10.1109\/DATE.2005.257"},{"key":"9035_CR36","doi-asserted-by":"crossref","unstructured":"Manolios, P., Srinivasan, S.: Verification of executable pipelined machines with bit-level interfaces. In: International Conference on Computer-Aided Design \u2013 ICCAD'05, pp. 855\u2013862 (2005c)","DOI":"10.1109\/ICCAD.2005.1560182"},{"key":"9035_CR37","unstructured":"Matthews, J., Vroon, D.: Partial clock functions in ACL2. In: Kaufmann, M., Moore, J.S. (eds.) Fifth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2004). See URL http:\/\/www.cs.utexas.edu\/users\/-moore\/acl2\/workshop-2004\/ (2004)"},{"key":"9035_CR38","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1990","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs, New Jersey (1990)"},{"key":"9035_CR39","doi-asserted-by":"crossref","unstructured":"Moore, J.S.: Inductive assertions and operational semantics. In: Advanced Research Working Conference on Correct Hardware Design and Verification Methods \u2013 CHARME'03, Vol. 2860 of Lecture Notes in Computer Science, pp. 289\u2013303 (2003)","DOI":"10.1007\/978-3-540-39724-3_27"},{"key":"9035_CR40","doi-asserted-by":"crossref","unstructured":"Namjoshi, K.S.: A simple characterization of stuttering bisimulation. In: 17th Conference on Foundations of Software Technology and Theoretical Computer Science, Vol. 1346 of LNCS, pp. 284\u2013296 (1997)","DOI":"10.1007\/BFb0058037"},{"issue":"4","key":"9035_CR41","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1023\/A:1010027404223","volume":"11","author":"J.C. Reynolds","year":"1998","unstructured":"Reynolds, J.C.: Definitional interpreters for higher-order programming languages. Higher-Order and Symbolic Computation 11(4), 363\u2013397 (1998). Reprinted from the proceedings of the 25th ACM National Conference (1972), with a foreword","journal-title":"Higher-Order and Symbolic Computation"},{"key":"9035_CR42","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1112\/S1461157000000176","volume":"1","author":"D.M. Russinoff","year":"1998","unstructured":"Russinoff, D.M.: A mechanically checked proof of IEEE compliance of a register-transfer-level specification of the AMD-K7 floating-point multiplication, division, and square root instructions. LMS J. Comput. Math. 1, 148\u2013200 (1998)","journal-title":"LMS J. Comput. Math."},{"key":"9035_CR43","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1023\/A:1008669628911","volume":"14","author":"D.M. Russinoff","year":"1999","unstructured":"Russinoff, D.M.: A mechanically checked proof of correctness of the AMD-K5 floating-point square root microcode. Form. Methods Syst. Des. 14, 75\u2013125 (1999)","journal-title":"Form. Methods Syst. Des."},{"key":"9035_CR44","unstructured":"Ryan, L.: Siege homepage. See URL http:\/\/www.cs.sfu.ca\/~loryan\/personal"},{"key":"9035_CR45","doi-asserted-by":"crossref","unstructured":"Sawada, J.: Formal verification of divide and square root algorithms using series calculation. In: Kaufmann, M., Moore, J.S. (eds.) Proceedings of the ACL2 Workshop 2002 (2002)","DOI":"10.1007\/3-540-36126-X_17"},{"key":"9035_CR46","unstructured":"Semiconductor Industry Association: International Technology Roadmap for Semiconductors. See URL http:\/\/public.itrs.net\/ (2004)"},{"key":"9035_CR47","unstructured":"Seshia, S., Lahiri, S., Bryant, R.: A User's Guide to UCLID version 1.0. See URL http:\/\/www.cs.cmu.edu\/uclid\/userguide.ps (2003a)"},{"key":"9035_CR48","doi-asserted-by":"crossref","unstructured":"Seshia, S.A., Lahiri, S.K., Bryant, R.E.: A hybrid SAT-based decision procedure for separation logic with uninterpreted functions. In: Design Automation Conference \u2013 DAC'03, pp. 425\u2013430 (2003b)","DOI":"10.1145\/775832.775945"},{"key":"9035_CR49","unstructured":"Smith, S., Perez, R., Weingart, S., Austel, V.: Validating a high-performance, programmable secure coprocessor. In: 22nd National Information Systems Security Conference (1999)"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-006-9035-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-006-9035-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-006-9035-0","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,11]],"date-time":"2025-01-11T08:52:41Z","timestamp":1736585561000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-006-9035-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,10,7]]},"references-count":49,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2007,1,17]]}},"alternative-id":["9035"],"URL":"https:\/\/doi.org\/10.1007\/s10817-006-9035-0","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2006,10,7]]}}}