{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:30:08Z","timestamp":1754483408124},"publisher-location":"Berlin, Heidelberg","reference-count":18,"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\/bfb0031822","type":"book-chapter","created":{"date-parts":[[2005,12,11]],"date-time":"2005-12-11T06:59:01Z","timestamp":1134284341000},"page":"377-388","source":"Crossref","is-referenced-by-count":13,"title":["Automatic generation of invariants in processor verification"],"prefix":"10.1007","author":[{"given":"Jeffrey X.","family":"Su","sequence":"first","affiliation":[]},{"given":"David L.","family":"Dill","sequence":"additional","affiliation":[]},{"given":"Clark W.","family":"Barrett","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,25]]},"reference":[{"key":"27_CR1","doi-asserted-by":"crossref","unstructured":"J. Burch and D. Dill, \u201cSymbolic Verification of Pipelined Microprocessor Control\u201d, 6th Computer Aided Verification, 1994.","DOI":"10.1007\/3-540-58179-0_44"},{"key":"27_CR2","unstructured":"J. Burch, E. Clarke, K. McMillan, D. Dill, and L. Hwang, \u201cSymbolic Model Checking: 1020 States and Beyond\u201d, 5th Annual IEEE Symposium on Logic In Computer Science, 1990."},{"key":"27_CR3","doi-asserted-by":"crossref","unstructured":"A. Cohn, \u201cA Proof of Correctness of the VIPER Microprocessors: The First Level\u201d, In VLSI Specification, Verification and Synthesis, 1988.","DOI":"10.1007\/978-1-4613-2007-4_2"},{"key":"27_CR4","unstructured":"D. Cyrluk, \u201cMicroprocessor Verification in PVS: A Methodology and Simple Example\u201d, Technical Report SRI-CSL-93-12, SRI Computer Science Laboratory, Dec. 1993."},{"key":"27_CR5","unstructured":"J. Hennessy and D. Patterson, \u201cComputer Architecture: A Quantitative Approach\u201d, Morgan Kaufmann, 1990."},{"key":"27_CR6","doi-asserted-by":"crossref","first-page":"429","DOI":"10.1007\/BF00243132","volume":"5","author":"W. Hunt Jr.","year":"1989","unstructured":"W. Hunt, Jr., \u201cMicroprocessor Design Verification\u201d, Journal of Automated Reasoning 5: p429\u2013460, 1989.","journal-title":"Journal of Automated Reasoning"},{"key":"27_CR7","doi-asserted-by":"crossref","unstructured":"R. Jones, D. Dill and J. Burch, \u201cEfficient Validity Checking for Processor Verification\u201d, IEEE\/ACM International Conference on Computer Aided Design, 1995.","DOI":"10.1109\/ICCAD.1995.479877"},{"key":"27_CR8","unstructured":"J. Joyce, G. Birtwistle, and M. Gordon, \u201cProving a Computer Correct in Higher Order Logic\u201d, Technical Report 100, Computer Lab., University of Cambridge, 1986."},{"key":"27_CR9","unstructured":"M. Langevin and E. Cerny, \u201cVerification of Processor-like Circuits\u201d, In Advanced Research Workshop on Correct Hardware Design Methodologies, June 1991."},{"key":"27_CR10","volume-title":"Technique Report, STAN-CS-TR-94","author":"Z. Manna","year":"1994","unstructured":"Z. Manna, et al., \u201cSTeP: the Stanford Temporal Prover\u201d, Technique Report, STAN-CS-TR-94, Computer Science Department, Stanford, 1994."},{"key":"27_CR11","unstructured":"Z. Manna and R. Waldinger, \u201cThe Deductive Foundations of Computer Programming\u201d, Addison Wesley, 1993."},{"key":"27_CR12","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli, \u201cTemporal Verification of Reactive Systems: Safety\u201d, Springer-Verlag, 1995.","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"27_CR13","unstructured":"S. Bensalem, Y. Lakhnech, and H. Saldi, \u201cPowerful Techniques for the Automatic Generation of Invariants\u201d, To appear in CAV96."},{"issue":"2","key":"27_CR14","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"A. Roscoe","year":"1979","unstructured":"A. Roscoe, \u201cOccam in the Specification and Verification of Microprocessors\u201d, ACM Trans. Prog. Lang. Syst., 1(2):245\u2013257, Oct. 1979.","journal-title":"ACM Trans. Prog. Lang. Syst."},{"key":"27_CR15","unstructured":"J. Saxe, S. Garland, J. Guttag, and J. Horning, \u201cUsing Transformations and Verification in Circuit Design\u201d, Technical Report 78, DEC System Research Center, Sept. 1991."},{"key":"27_CR16","unstructured":"R. Simoni, \u201cPP Instruction Set Architecture Specification\u201d, version 1.7, Stanford FLASH group, 1995"},{"issue":"5","key":"27_CR17","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1109\/52.57892","volume":"7","author":"M. Srivas","year":"1990","unstructured":"M. Srivas and M. Brickford, \u201cFormal Verification of a Pipelined Microprocessor\u201d, IEEE Software, 7(5):52\u201364, Sept. 1990.","journal-title":"IEEE Software"},{"key":"27_CR18","doi-asserted-by":"crossref","unstructured":"C. Barrett, D. Dill, and J. Levitt, \u201cValidity Checking for Combinations of Theories with Equality\u201d, To appear in FMCAD, 1996.","DOI":"10.1007\/BFb0031808"}],"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\/BFb0031822","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T13:50:03Z","timestamp":1586613003000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0031822"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540619376","9783540495673"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/bfb0031822","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}