{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,31]],"date-time":"2025-01-31T12:40:27Z","timestamp":1738327227442,"version":"3.35.0"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540691471"},{"type":"electronic","value":"9783540691495"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"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":[[2008]]},"DOI":"10.1007\/978-3-540-69149-5_47","type":"book-chapter","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T16:07:43Z","timestamp":1218557263000},"page":"438-447","source":"Crossref","is-referenced-by-count":0,"title":["The Challenge of Hardware-Software Co-verification"],"prefix":"10.1007","author":[{"given":"Panagiotis","family":"Manolios","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"47_CR1","first-page":"83","volume-title":"Machine intelligence","author":"R.S. Boyer","year":"1988","unstructured":"Boyer, R.S., Moore, J.S.: Integrating decision procedures into heuristic theorem provers: a case study of linear arithmetic. In: Machine intelligence, vol.\u00a011, pp. 83\u2013124. Oxford University Press, Inc. Oxford (1988)"},{"key":"47_CR2","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":"47_CR3","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.: 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":"47_CR4","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":"47_CR5","unstructured":"Dijkstra, E.W.: Science fiction and science reality in computing, EWD 952 (1986), http:\/\/www.cs.utexas.edu\/sers\/EWD"},{"key":"47_CR6","doi-asserted-by":"crossref","unstructured":"Greve, D., Wilding, M., Hardin, D.: High-speed, analyzable simulators. In: Kaufmann et al., (eds.), [8] pp. 113\u2013135.","DOI":"10.1007\/978-1-4757-3188-0_8"},{"issue":"1","key":"47_CR7","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1145\/602382.602403","volume":"50","author":"T. Hoare","year":"2003","unstructured":"Hoare, T.: The verifying compiler: A grand challenge for computing research. J. ACM\u00a050(1), 63\u201369 (2003)","journal-title":"J. ACM"},{"volume-title":"Computer-Aided Reasoning: ACL2 Case Studies","year":"2000","key":"47_CR8","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S. (eds.): Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Publishers, Dordrecht (2000)"},{"key":"47_CR9","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":"47_CR10","doi-asserted-by":"crossref","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S.: Supporting files for Computer-Aided Reasoning: ACL2 Case Studies (2000), http:\/\/www.cs.utexas.edu\/users\/moore\/acl2","DOI":"10.1007\/978-1-4615-4449-4"},{"key":"47_CR11","unstructured":"Kaufmann, M., Moore, J.S.: ACL2, http:\/\/www.cs.utexas.edu\/users\/moore\/acl2"},{"key":"47_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/3-540-36126-X_9","volume-title":"Formal Methods in Computer-Aided Design","author":"S. Lahiri","year":"2002","unstructured":"Lahiri, S., Seshia, S., Bryant, R.: Modeling and verification of out-of-order microprocessors using UCLID. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517, pp. 142\u2013159. Springer, Heidelberg (2002)"},{"key":"47_CR13","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":"47_CR14","unstructured":"Manolios, P.: Mechanical Verification of Reactive Systems. PhD thesis, University of Texas at Austin (August, 2001), http:\/\/www.cc.gatech.edu\/~manolios-publications.html"},{"key":"47_CR15","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":"47_CR16","unstructured":"Manolios, P., Srinivasan, S.: A parameterized benchmark suite of hard pipelined-machine-verification problems"},{"key":"47_CR17","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":"47_CR18","unstructured":"P.\u00a0Manolios and S.\u00a0Srinivasan. A suite of hard ACL2 theorems arising in refinement-based processor verification. In M.\u00a0Kaufmann and J.\u00a0S. Moore, (eds.), Fifth International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2-2004) (November, 2004) http:\/\/www.cs.utexas.edu\/users\/moore\/acl2\/workshop-2004\/"},{"key":"47_CR19","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 (to appear, 2005)","DOI":"10.1109\/ICCAD.2005.1560183"},{"key":"47_CR20","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":"47_CR21","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":"47_CR22","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 (to appear, 2005)","DOI":"10.1109\/ICCAD.2005.1560182"},{"key":"47_CR23","volume-title":"Communication and Concurrency","author":"R. Milner","year":"1990","unstructured":"Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1990)"},{"key":"47_CR24","doi-asserted-by":"crossref","unstructured":"Moore, J.S.: Special issue on system verification. Journal of Automated Reasoning\u00a05(4) (1989)","DOI":"10.1007\/BF00243130"},{"key":"47_CR25","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":"47_CR26","doi-asserted-by":"crossref","unstructured":"Russinoff, D.M., Flatau, A.: RTL verification: A floating-point multiplier. In: Kaufmann et\u00a0al (eds.), [8], pp. 201\u2013231","DOI":"10.1007\/978-1-4757-3188-0_13"},{"key":"47_CR27","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1145\/337292.337331","volume-title":"Proceedings of the 37th conference on Design Automation","author":"M.N. Velev","year":"2000","unstructured":"Velev, M.N., Bryant, R.E.: Formal verification of superscalar microprocessors with multicycle functional units, exceptions, and branch prediction. In: Proceedings of the 37th conference on Design Automation, pp. 112\u2013117. ACM Press, New York (2000)"}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69149-5_47","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,31]],"date-time":"2025-01-31T11:58:40Z","timestamp":1738324720000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69149-5_47"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540691471","9783540691495"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69149-5_47","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}