{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,6]],"date-time":"2026-04-06T21:57:44Z","timestamp":1775512664613,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":59,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540343042","type":"print"},{"value":"9783540343059","type":"electronic"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"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":[[2006]]},"DOI":"10.1007\/11757283_7","type":"book-chapter","created":{"date-parts":[[2006,11,27]],"date-time":"2006-11-27T13:02:12Z","timestamp":1164632532000},"page":"176-210","source":"Crossref","is-referenced-by-count":3,"title":["Refinement and Theorem Proving"],"prefix":"10.1007","author":[{"given":"Panagiotis","family":"Manolios","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","doi-asserted-by":"crossref","unstructured":"Bentley, B.: Validating the Intel Pentium 4 microprocessor. In: 38th Design Automation Conference, pp. 253\u2013255 (2001)","DOI":"10.1145\/378239.378473"},{"key":"7_CR2","doi-asserted-by":"crossref","unstructured":"Bentley, B.: Validating a modern microprocessor (2005), see: http:\/\/www.cav2005.inf.ed.ac.uk\/bentleyCAV07082005.ppt","DOI":"10.1007\/11513988_2"},{"key":"7_CR3","doi-asserted-by":"crossref","unstructured":"Bertoli, P., Traverso, P.: Design verification of a safety-critical embedded verifier. In: Kaufmann, et al. (eds.) [22], pp. 233\u2013245","DOI":"10.1007\/978-1-4757-3188-0_14"},{"key":"7_CR4","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1016\/B978-0-12-450010-5.50007-4","volume-title":"Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy","author":"R.S. Boyer","year":"1991","unstructured":"Boyer, R.S., Goldschlag, D.M., Kaufmann, M., Moore, J.S.: Functional instantiation in first order logic. In: Lifschitz, V. (ed.) Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, pp. 7\u201326. Academic Press, London (1991)"},{"key":"7_CR5","volume-title":"A Computational Logic Handbook","author":"R.S. Boyer","year":"1997","unstructured":"Boyer, R.S., Moore, J.S.: A Computational Logic Handbook, 2nd edn. Academic Press, London (1997)","edition":"2"},{"key":"7_CR6","unstructured":"Boyer, R.S., Moore, J.S.: Single-threaded objects in ACL2 (1999), see: http:\/\/www.cs.utexas.edu\/users\/moore\/publications\/acl2-papers.html#Foundations"},{"key":"7_CR7","first-page":"31","volume-title":"1997 IEEE International Conference on Computer Design","author":"B. Brock","year":"1997","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. IEEE Computer Society, Los Alamitos (1997)"},{"key":"7_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BFb0031816","volume-title":"Formal Methods in Computer-Aided Design","author":"B. Brock","year":"1996","unstructured":"Brock, B., Kaufmann, M., Moore, J.S.: ACL2 theorems about commercial microprocessors. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 275\u2013293. Springer, Heidelberg (1996)"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Browne, M., Clarke, E.M., Grumberg, O.: Characterizing finite Kripke structures in propositional temporal logic. Theoretical Computer Science\u00a059 (1988)","DOI":"10.1016\/0304-3975(88)90098-9"},{"key":"7_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/3-540-45657-0_7","volume-title":"Computer Aided Verification","author":"R.E. Bryant","year":"2002","unstructured":"Bryant, R.E., Lahiri, S.K., Seshia, S.A.: Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 78\u201392. Springer, Heidelberg (2002)"},{"key":"7_CR11","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":"J.R. 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.\u00a0818, pp. 68\u201380. Springer, Heidelberg (1994)"},{"key":"7_CR12","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"7_CR13","unstructured":"Dillinger, P., Manolios, P., Moore, J.S., Vroon, D.: ACL2E homepage, see: http:\/\/www.cc.gatech.edu\/home\/manolios\/acl2s"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Greve, D., Wilding, M., Hardin, D.: High-speed, analyzable simulators. In: Kaufmann, et al. (eds.) [22], pp. 113\u2013135","DOI":"10.1007\/978-1-4757-3188-0_8"},{"key":"7_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/3-540-49519-3_21","volume-title":"Formal Methods in Computer-Aided Design","author":"D.A. Greve","year":"1998","unstructured":"Greve, D.A.: Symbolic simulation of the JEM1 microprocessor. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol.\u00a01522, pp. 321\u2013333. Springer, Heidelberg (1998)"},{"key":"7_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0028729","volume-title":"Computer Aided Verification","author":"D. Hardin","year":"1998","unstructured":"Hardin, D., Wilding, M., Greve, D.: Transforming the theorem prover into a digital design tool: From concept car to off-road vehicle. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, Springer, Heidelberg (1998), http:\/\/pobox.com\/users\/hokie\/docs\/concept.ps"},{"key":"7_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/978-3-540-39724-3_29","volume-title":"Correct Hardware Design and Verification Methods","author":"W. Hunt","year":"2003","unstructured":"Hunt, W., Krug, R., Moore, J.S.: The addition of non-linear arithmetic to ACL2. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol.\u00a02860, pp. 319\u2013333. Springer, Heidelberg (2003)"},{"issue":"4","key":"7_CR18","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1007\/BF00243132","volume":"5","author":"W.A. Hunt Jr.","year":"1989","unstructured":"Hunt Jr., W.A.: Microprocessor design verification. Journal of Automated Reasoning\u00a05(4), 429\u2013460 (1989)","journal-title":"Journal of Automated Reasoning"},{"key":"7_CR19","unstructured":"Hunt Jr., W.A., Brock, B.: A formal HDL and its use in the FM9001 verification. In: Proceedings of the Royal Society (1992)"},{"key":"7_CR20","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1023\/A:1008685826293","volume":"11","author":"W.A. Hunt Jr.","year":"1997","unstructured":"Hunt Jr., W.A., Brock, B.: The DUAL-EVAL hardware description language and its use in the formal specification and verification of the FM9001 microprocessor. Formal Methods in Systems Design\u00a011, 71\u2013105 (1997)","journal-title":"Formal Methods in Systems Design"},{"key":"7_CR21","doi-asserted-by":"crossref","unstructured":"Kane, R., Manolios, P., Srinivasan, S.K.: Monolithic verification of deep pipelines with collapsed flushing. In: Design Automation and Test in Europe, DATE 2006 (2006)","DOI":"10.1109\/DATE.2006.244077"},{"key":"7_CR22","volume-title":"Computer-Aided Reasoning: ACL2 Case Studies","year":"2000","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S. (eds.): Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Publishers, Dordrecht (2000)"},{"key":"7_CR23","volume-title":"Computer-Aided Reasoning: An Approach","author":"M. Kaufmann","year":"2000","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Dordrecht (2000)"},{"key":"7_CR24","doi-asserted-by":"crossref","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S.: Supporting files for Computer-Aided Reasoning: ACL2 Case Studies (2000), see the link from: http:\/\/www.cs.utexas.edu\/users\/moore\/acl2","DOI":"10.1007\/978-1-4757-3188-0"},{"key":"7_CR25","doi-asserted-by":"crossref","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S.: Supporting files for Computer-Aided Reasoning: An Approach (2000), see the link from: http:\/\/www.cs.utexas.edu\/users\/moore\/acl2","DOI":"10.1007\/978-1-4757-3188-0"},{"key":"7_CR26","unstructured":"Kaufmann, M., Moore, J.S.: ACL2 homepage, see: http:\/\/www.cs.utexas.edu\/users\/moore\/acl2"},{"key":"7_CR27","unstructured":"Kaufmann, M., Moore, J.S.: A precise description of the ACL2 logic. Technical report, Department of Computer Sciences, University of Texas at Austin (1997), see: http:\/\/www.cs.utexas.edu\/users\/moore\/publications\/acl2-papers.html#Foundations"},{"key":"7_CR28","unstructured":"Kaufmann, M., Moore, J.S. (eds.): Proceedings of the ACL2 Workshop 2000. The University of Texas at Austin, Technical Report TR-00-29 (November 2000)"},{"issue":"2","key":"7_CR29","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1023\/A:1026517200045","volume":"26","author":"M. Kaufmann","year":"2001","unstructured":"Kaufmann, M., Moore, J.S.: Structured theory development for a mechanized logic. Journal of Automated Reasoning\u00a026(2), 161\u2013203 (2001)","journal-title":"Journal of Automated Reasoning"},{"key":"7_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1007\/3-540-40922-X_11","volume-title":"Formal Methods in Computer-Aided Design","author":"P. Manolios","year":"2000","unstructured":"Manolios, P.: Correctness of pipelined machines. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 161\u2013178. Springer, Heidelberg (2000)"},{"key":"7_CR31","unstructured":"Manolios, P.: Verification of pipelined machines in ACL2. In: Kaufmann, Moore [28]"},{"key":"7_CR32","unstructured":"Manolios, P.: Mechanical Verification of Reactive Systems. PhD thesis, University of Texas at Austin (August 2001), see: http:\/\/www.cc.gatech.edu\/~manolios\/publications.html"},{"key":"7_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-540-39724-3_28","volume-title":"Correct Hardware Design and Verification Methods","author":"P. Manolios","year":"2003","unstructured":"Manolios, P.: A compositional theory of refinement for branching time. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol.\u00a02860, pp. 304\u2013318. Springer, Heidelberg (2003)"},{"key":"7_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/3-540-48683-6_32","volume-title":"Computer Aided Verification","author":"P. Manolios","year":"1999","unstructured":"Manolios, P., Namjoshi, K.S., Sumners, R.: Linking theorem proving and model-checking with well-founded bisimulation. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 369\u2013379. Springer, Heidelberg (1999)"},{"key":"7_CR35","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, DATE 2004, pp. 168\u2013175 (2004)","DOI":"10.1109\/DATE.2004.1268844"},{"key":"7_CR36","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) (November 2004), see: http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/workshop-2004\/"},{"key":"7_CR37","doi-asserted-by":"crossref","unstructured":"Manolios, P., Srinivasan, S.: A complete compositional reasoning framework for the efficient verification of pipelined machines. In: ICCAD 2005, International Conference on Computer-Aided Design (2005)","DOI":"10.1109\/ICCAD.2005.1560183"},{"key":"7_CR38","unstructured":"Manolios, P., Srinivasan, S.: A computationally efficient method based on commitment refinement maps for verifying pipelined machines models. In: ACM-IEEE International Conference on Formal Methods and Models for Codesign, pp. 189\u2013198 (2005)"},{"key":"7_CR39","doi-asserted-by":"crossref","unstructured":"Manolios, P., Srinivasan, S.: Refinement maps for efficient verification of processor models. In: Design Automation and Test in Europe, DATE 2005, pp. 1304\u20131309 (2005)","DOI":"10.1109\/DATE.2005.257"},{"key":"7_CR40","doi-asserted-by":"crossref","unstructured":"Manolios, P., Srinivasan, S.: Verification of executable pipelined machines with bit-level interfaces. In: ICCAD-2005, International Conference on Computer-Aided Design (2005)","DOI":"10.1109\/ICCAD.2005.1560182"},{"key":"7_CR41","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-540-45085-6_19","volume-title":"Automated Deduction \u2013 CADE-19","author":"P. Manolios","year":"2003","unstructured":"Manolios, P., Vroon, D.: Algorithms for ordinal arithmetic. In: Baader, F. (ed.) CADE 2003. LNCS (LNAI), vol.\u00a02741, pp. 243\u2013258. Springer, Heidelberg (2003)"},{"key":"7_CR42","unstructured":"Manolios, P., Vroon, D.: Ordinal arithmetic in ACL2. In: Kaufmann, M., Moore, J.S. (eds.) Fourth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2003) (July 2003), see: http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/workshop-2003\/"},{"key":"7_CR43","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/978-3-540-30494-4_7","volume-title":"Formal Methods in Computer-Aided Design","author":"P. Manolios","year":"2004","unstructured":"Manolios, P., Vroon, D.: Integrating reasoning about ordinal arithmetic into ACL2. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 82\u201397. Springer, Heidelberg (2004)"},{"key":"7_CR44","doi-asserted-by":"crossref","unstructured":"Manolios, P., Vroon, D.: Ordinal arithmetic: Algorithms and mechanization. Journal of Automated Reasoning (to appear, 2006)","DOI":"10.1007\/s10817-005-9023-9"},{"key":"7_CR45","doi-asserted-by":"crossref","unstructured":"Manolios, P., Vroon, D.: Termination analysis with calling context graphs (submitted, 2006)","DOI":"10.1007\/11817963_36"},{"key":"7_CR46","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1990","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1990)"},{"key":"7_CR47","volume-title":"Piton : A Mechanically Verified Assembly-Level Language","author":"J.S. Moore","year":"1996","unstructured":"Moore, J.S.: Piton: A Mechanically Verified Assembly-Level Language. Kluwer Academic Press, Dordrecht (1996)"},{"issue":"9","key":"7_CR48","doi-asserted-by":"publisher","first-page":"913","DOI":"10.1109\/12.713311","volume":"47","author":"J.S. Moore","year":"1998","unstructured":"Moore, J.S., Lynch, T., Kaufmann, M.: A mechanically checked proof of the AMD5 K 86 floating-point division program. IEEE Trans. Comp.\u00a047(9), 913\u2013926 (1998)","journal-title":"IEEE Trans. Comp."},{"key":"7_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/BFb0058037","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"K.S. Namjoshi","year":"1997","unstructured":"Namjoshi, K.S.: A simple characterization of stuttering bisimulation. In: Ramesh, S., Sivakumar, G. (eds.) FST TCS 1997. LNCS, vol.\u00a01346, pp. 284\u2013296. Springer, Heidelberg (1997)"},{"key":"7_CR50","unstructured":"Russinoff, D.M.: A mechanically checked proof of correctness of the AMD5 K 86 floating-point square root microcode. Formal Methods in System Design Special Issue on Arithmetic Circuits (1997)"},{"key":"7_CR51","first-page":"148","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. London Mathematical Society Journal of Computation and Mathematics\u00a01, 148\u2013200 (1998)","journal-title":"London Mathematical Society Journal of Computation and Mathematics"},{"key":"7_CR52","doi-asserted-by":"publisher","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. Formal Methods in System Design\u00a014, 75\u2013125 (1999)","journal-title":"Formal Methods in System Design"},{"key":"7_CR53","doi-asserted-by":"crossref","unstructured":"Russinoff, D.M., Flatau, A.: RTL verification: A floating-point multiplier. In: Kaufmann, et al. (eds.) [22], pp. 201\u2013231","DOI":"10.1007\/978-1-4757-3188-0_13"},{"key":"7_CR54","doi-asserted-by":"crossref","unstructured":"Sawada, J.: Formal Verification of an Advanced Pipelined Machine. PhD thesis, University of Texas at Austin (December 1999), see: http:\/\/www.cs.utexas.edu\/users\/sawada\/dissertation\/","DOI":"10.1007\/978-1-4757-3188-0_9"},{"key":"7_CR55","doi-asserted-by":"crossref","unstructured":"Sawada, J.: Verification of a simple pipelined machine model. In: Kaufmann, et al. (eds.) [22], pp. 137\u2013150","DOI":"10.1007\/978-1-4757-3188-0_9"},{"key":"7_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/3-540-63166-6_36","volume-title":"Computer Aided Verification","author":"J. Sawada","year":"1997","unstructured":"Sawada, J., Hunt Jr., W.A.: Trace table based approach for pipelined microprocessor verification. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 364\u2013375. Springer, Heidelberg (1997)"},{"key":"7_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/BFb0028740","volume-title":"Computer Aided Verification","author":"J. Sawada","year":"1998","unstructured":"Sawada, J., Hunt Jr., W.A.: Processor verification with precise exceptions and speculative execution. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 135\u2013146. Springer, Heidelberg (1998)"},{"key":"7_CR58","unstructured":"International technology roadmap for semiconductors (2004), see: http:\/\/public.itrs.net\/"},{"key":"7_CR59","volume-title":"Common Lisp The Language","author":"G.L. Steele Jr.","year":"1990","unstructured":"Steele Jr., G.L.: Common Lisp The Language, 2nd edn. Digital Press, Burlington (1990)","edition":"2"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Hardware Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11757283_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,12]],"date-time":"2025-01-12T04:41:58Z","timestamp":1736656918000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11757283_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540343042","9783540343059"],"references-count":59,"URL":"https:\/\/doi.org\/10.1007\/11757283_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}