{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,4]],"date-time":"2026-05-04T10:36:36Z","timestamp":1777890996488,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540581796","type":"print"},{"value":"9783540484691","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58179-0_44","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T10:25:55Z","timestamp":1330251955000},"page":"68-80","source":"Crossref","is-referenced-by-count":211,"title":["Automatic verification of pipelined microprocessor control"],"prefix":"10.1007","author":[{"given":"Jerry R.","family":"Burch","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David L.","family":"Dill","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"6_CR1","unstructured":"D. L. Beatty. A Methodology for Formal Hardware Verification, with Application to Microprocessors. PhD thesis, School of Computer Science, Carnegie Mellon University, Aug. 1993."},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"K. S. Brace, R. L. Rudell, and R. E. Bryant. Efficient implementation of a BDD package. In 27th ACM\/IEEE Design Automation Conference, 1990.","DOI":"10.1145\/123186.123222"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"R. E. Bryant, D. L. Beatty, and C.-J. H. Seger. Formal hardware verification by symbolic ternary trajectory evaluation. In 28th ACM\/IEEE Design Automation Conference, 1991.","DOI":"10.1145\/127601.127701"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"J. R. Burch, E. M. Clarke, and D. E. Long. Representing circuits more efficiently in symbolic model checking. In 28th ACM\/IEEE Design Automation Conference, 1991.","DOI":"10.1145\/127601.127702"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"J. R. Burch, E. M. Clarke, K. L. McMillan, and D. L. Dill. Sequential circuit verification using symbolic model checking. In 27th ACM\/IEEE Design Automation Conference, 1990.","DOI":"10.1145\/123186.123223"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, O. Grumberg, and D. E. Long. Model checking and abstraction. In Nineteenth Annual ACM Symposium on Principles on Programming Languages, 1992.","DOI":"10.1145\/143165.143235"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"A. J. Cohn. A proof of correctness of the Viper microprocessors: The first level. In G. Birtwistle and P. A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis, pages 27\u201372. Kluwer, 1988.","DOI":"10.1007\/978-1-4613-2007-4_2"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"A. J. Cohn. Correctness properties of the Viper block model: The second level. In G. Birtwistle, editor, Proceedings of the 1988 Design Verification Conference. Springer-Verlag, 1989. Also published as University of Cambridge Computer Laboratory Technical Report No. 134.","DOI":"10.1007\/978-1-4612-3658-0_1"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"F. Corella. Automated high-level verification against clocked algorithmic specifications. Technical Report RC 18506, IBM Research Division, Nov. 1992.","DOI":"10.1016\/B978-0-444-81641-2.50017-4"},{"key":"6_CR10","volume-title":"Automatic high-level verification against clocked algorithmic specifications","author":"F. Corella","year":"1993","unstructured":"F. Corella. Automatic high-level verification against clocked algorithmic specifications. In Proceedings of the IFIP WG10.2 Conference on Computer Hardware Description Languages and their Applications, Ottawa, Canada, Apr. 1993. Elsevier Science Publishers B.V."},{"key":"6_CR11","unstructured":"D. Cyrluk. Microprocessor verification in PVS: A methodology and simple example. Technical Report SRI-CSL-93-12, SRI Computer Science Laboratory, Dec. 1993."},{"key":"6_CR12","unstructured":"D. Detlefs and G. Nelson. Personal communication, 1994."},{"key":"6_CR13","unstructured":"J. L. Hennessy. Designing a computer as a microprocessor: Experience and lessons from the MIPS 4000. A lecture at the Symposium on Integrated Systems, Seattle, Washington, March 14, 1993."},{"key":"6_CR14","unstructured":"J. L. Hennessy and D. A. Patterson. Computer Architecture: A Quantitative Approach. Morgan Kaufmann, 1990."},{"key":"6_CR15","volume-title":"Technical Report 47","author":"W. A. Hunt Jr.","year":"1985","unstructured":"W. A. Hunt, Jr. FM8501: A verified microprocessor. Technical Report 47, University of Texas at Austin, Institute for Computing Science, Dec. 1985."},{"key":"6_CR16","unstructured":"J. Joyce, G. Birtwistle, and M. Gordon. Proving a computer correct in higher order logic. Technical Report 100, Computer Lab., University of Cambridge, 1986."},{"key":"6_CR17","unstructured":"M. Langevin and E. Cerny. Verification of processor-like circuits. In P. Prinetto and P. Camurati, editors, Advanced Research Workshop on Correct Hardware Design Methodologies, June 1991."},{"issue":"2","key":"6_CR18","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"G. Nelson and D. C. Oppen. Simplification by cooperating decision procedures. ACM Trans. Prog. Lang. Syst., 1(2):245\u2013257, Oct. 1979.","journal-title":"ACM Trans. Prog. Lang. Syst."},{"issue":"1652","key":"6_CR19","doi-asserted-by":"crossref","first-page":"137","DOI":"10.1098\/rsta.1992.0030","volume":"339","author":"A. W. Roscoe","year":"1992","unstructured":"A. W. Roscoe. Occam in the specification and verification of microprocessors. Philosophical Transactions of the Royal Society of London, Series A: Physical Sciences and Engineering, 339(1652):137\u2013151, Apr. 15, 1992.","journal-title":"Philosophical Transactions of the Royal Society of London, Series A: Physical Sciences and Engineering"},{"key":"6_CR20","unstructured":"J. B. Saxe, S. J. Garland, J. V. Guttag, and J. J. Horning. Using transformations and verification in circuit design. Technical Report 78, DEC Systems Research Center, Sept. 1991."},{"issue":"2","key":"6_CR21","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1145\/322123.322137","volume":"26","author":"R. E. Shostak","year":"1979","unstructured":"R. E. Shostak. A practical decision procedure for arithmetic with function symbols. J. ACM, 26(2):351\u2013360, Apr. 1979.","journal-title":"J. ACM"},{"issue":"5","key":"6_CR22","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1109\/52.57892","volume":"7","author":"M. Srivas","year":"1990","unstructured":"M. Srivas and M. Bickford. Formal verification of a pipelined microprocessor. IEEE Software, 7(5):52\u201364, Sept. 1990.","journal-title":"IEEE Software"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58179-0_44.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:17:50Z","timestamp":1605629870000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58179-0_44"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540581796","9783540484691"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-58179-0_44","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994]]}}}