{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:41:11Z","timestamp":1754484071692},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540619376"},{"type":"electronic","value":"9783540495673"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/bfb0031821","type":"book-chapter","created":{"date-parts":[[2005,12,11]],"date-time":"2005-12-11T06:59:01Z","timestamp":1134284341000},"page":"362-376","source":"Crossref","is-referenced-by-count":18,"title":["Mechanically checking a lemma used in an automatic verification tool"],"prefix":"10.1007","author":[{"given":"Phillip J.","family":"Windley","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jerry R.","family":"Burch","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,25]]},"reference":[{"key":"26_CR1","doi-asserted-by":"crossref","unstructured":"Jerry R. Burch and David L. Dill. Automatic verification of pipelined microprocessor control. In David L. Dill, editor, Conference on Computer-Aided Verification, volume 818 of Lecture Notes in Computer Science. Springer-Verlag, June 1994.","DOI":"10.1007\/3-540-58179-0_44"},{"key":"26_CR2","unstructured":"Derek L. Beatty. A Methodology for Formal Hardware Verification, with Application to Microprocessors. PhD thesis, School of Computer Science, Carnegie Mellon University, August 1993."},{"key":"26_CR3","doi-asserted-by":"crossref","unstructured":"Jerry R. Burch. Techniques for verifying superscalar microprocessors. In Design Automation Conference, June 1996.","DOI":"10.1145\/240518.240623"},{"key":"26_CR4","unstructured":"Albert Camilleri, Mike Gordon, and Tom Melham. Hardware verification using higher order logic. In D. Borrione, editor, From HDL Descriptions to Guaranteed Correct Circuit Designs. Elsevier Scientific Publishers, 1987."},{"key":"26_CR5","doi-asserted-by":"crossref","unstructured":"Alonzo Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5, 1940.","DOI":"10.2307\/2266170"},{"key":"26_CR6","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":"26_CR7","doi-asserted-by":"crossref","unstructured":"D. Cyrluk, S. Rajan, N. Shankar, and M. K. Srivas. Effective theorem proving for hardware verification. In Conference on Theorem Provers in Circuit Design, September 1994.","DOI":"10.1007\/3-540-59047-1_50"},{"key":"26_CR8","doi-asserted-by":"crossref","unstructured":"David Cyrluk. Inverting the abstraction mapping: A methodology for hardware verification. In Conference on Formal Methods in Computer-Aided Design, November 1996. (This volume).","DOI":"10.1007\/BFb0031807"},{"key":"26_CR9","doi-asserted-by":"crossref","unstructured":"Michael J. C. Gordon. HOL: A proof generating system for higher-order logic. In G. Birtwhistle and P. A. Subrahmanyam, editors, VLSI Specification, Verification, and Synthesis. Kluwer Academic Press, 1988.","DOI":"10.1007\/978-1-4613-2007-4_3"},{"key":"26_CR10","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, December 1985."},{"key":"26_CR11","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":"26_CR12","doi-asserted-by":"crossref","unstructured":"Robert B. Jones, David L. Dill, and Jerry R. Burch. Efficient validity checking for processor verification. In Intl. Conf. on Comp. Aided Design, 1995.","DOI":"10.1109\/ICCAD.1995.479877"},{"key":"26_CR13","doi-asserted-by":"crossref","unstructured":"Robert B. Jones, Carl-Johan H. Seger, and David L. Dill. Self-consistency checking. In Conference on Formal Methods in Computer-Aided Design, November 1996. (This volume).","DOI":"10.1007\/BFb0031806"},{"key":"26_CR14","doi-asserted-by":"crossref","unstructured":"Jeffrey Kuskin et al. The Stanford FLASH multiprocessor. In Intl. Symp. on Comp. Arch., 1994.","DOI":"10.1109\/ISCA.1994.288140"},{"issue":"5","key":"26_CR15","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1109\/52.57892","volume":"7","author":"M. Srivas","year":"1990","unstructured":"Mandayam Srivas and Mark Bickford. Formal verification of a pipelined microprocessor. IEEE Software, 7(5):52\u201364, September 1990.","journal-title":"IEEE Software"},{"key":"26_CR16","unstructured":"James B. Saxe, Stephen J. Garland, John V. Guttag, and James J. Horning. Using transformations and verification in circuit design. Technical Report 78, DEC Systems Research Center, September 1991."},{"key":"26_CR17","doi-asserted-by":"crossref","unstructured":"Mandayam Srivas and Steven P. Miller. Applying formal verification to a commercial microprocessor. In IFIP Conference on Hardware Description Languages (CHDL 95), Tokyo, Japan, August 1995.","DOI":"10.1109\/ASPDAC.1995.486361"},{"issue":"2","key":"26_CR18","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1007\/BF00122419","volume":"8","author":"M. Srivas","year":"1996","unstructured":"M. Srivas and S. P. Miller. Applying formal verification to the AAMP5 microprocessor: A case study in the industrial use of formal methods. Formal Methods in System Design, 8(2): 153\u201388, March 1996.","journal-title":"Formal Methods in System Design"},{"key":"26_CR19","unstructured":"Phillip J. Windley and Michael Coe. The formal verification of instruction pipelines. In Ramayya Kumar and Thomas Kropf, editors, Conference on Theorem Provers in Circuit Design, Lecture Notes in Computer Science. Springer-Verlag, September 1994."},{"key":"26_CR20","doi-asserted-by":"crossref","unstructured":"Phillip J. Windley. A theory of generic interpreters. In George J. Milne and Laurence Pierre, editors, Correct Hardware Design and Verification Methods, volume 683 of Lecture Notes in Computer Science, pages 122\u2013134. Springer-Verlag, June 1993.","DOI":"10.1007\/BFb0021719"},{"key":"26_CR21","doi-asserted-by":"crossref","unstructured":"Phillip J. Windley. Formal modeling and verification of microprocessors. IEEE Transactions on Computers, 44(1), January 1995.","DOI":"10.1109\/12.368009"},{"key":"26_CR22","unstructured":"Phillip J. Windley. Verifying pipelined microprocessors. In IFIP Conference on Hardware Description Languages (CHDL 95), Tokyo, Japan, August 1995."}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0031821","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T13:50:11Z","timestamp":1586613011000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0031821"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540619376","9783540495673"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/bfb0031821","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}