{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T06:39:58Z","timestamp":1768286398390,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540551799","type":"print"},{"value":"9783540467632","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1992]]},"DOI":"10.1007\/3-540-55179-4_35","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T09:51:51Z","timestamp":1330249911000},"page":"365-375","source":"Crossref","is-referenced-by-count":9,"title":["Automating most parts of hardware proofs in HOL"],"prefix":"10.1007","author":[{"given":"Klaus","family":"Schneider","sequence":"first","affiliation":[]},{"given":"Ramayya","family":"Kumar","sequence":"additional","affiliation":[]},{"given":"Thomas","family":"Kropf","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,29]]},"reference":[{"key":"35_CR1","unstructured":"M. J. C. Gordon: Why High-Order Logic is a good Formalism for Specifying and Verifying Hardware; Milne\/Subrahmanyam (Eds.), Formal Aspects of VLSI Design, Proc. Edinburgh Workshop on VLSI 1985, North-Holland 1986, pp. 153\u2013178."},{"key":"35_CR2","unstructured":"J. Joyce: More Reasons Why Higher-Order Logic is a Good Formalism for Specifiying and Verifying Hardware; Proc. International Workshop on Formal Methods in VLSI Design, Miami, January 1991."},{"key":"35_CR3","first-page":"43","volume-title":"Proc. IFIP Workshop on \u201cFrom H.D.L. Descriptions to Guaranteed Correct Circuit Design\u201d","author":"A. Camilleri","year":"1986","unstructured":"A. Camilleri, M. J. C. Gordon, T. Melham: Hardware Verification using Higher-Order Logic; Borrione (Ed.), Proc. IFIP Workshop on \u201cFrom H.D.L. Descriptions to Guaranteed Correct Circuit Design\u201d, Grenoble 1986, North-Holland, pp. 43\u201367."},{"key":"35_CR4","unstructured":"S. Finn, M. Fourman, M. Francis, B. Harris: Formal System Design \u2014 Interactive Synthesis based on Computer Assisted Formal Reasoning; Proc. Intl. Workshop on Applied Formal Methods for Correct VLSI Design, Leuven, Nov. 1989."},{"issue":"No.3","key":"35_CR5","first-page":"242","volume":"133","author":"F. K. Hanna","year":"1986","unstructured":"F.K. Hanna, N. Daeche: Specification and Verification of Digital Systems Using Higher-Order Predicate Logic; IEE Proc. Pt. E, Vol. 133, No. 3, September 1986, pp. 242\u2013254.","journal-title":"IEE Proc."},{"key":"35_CR6","doi-asserted-by":"crossref","unstructured":"A. Cohn: Correctness Properties of the Viper Block Model: The Second Level; Current Trends in Hardware Verification and Automated Theorem Proving, Springer Verlag, 1988.","DOI":"10.1007\/978-1-4612-3658-0_1"},{"key":"35_CR7","doi-asserted-by":"crossref","unstructured":"W.J. Cullyer: Implementing Safety Critical Systems: The VIPER Microprocessor; VLSI Specification, Verification and Synthesis, Eds. Birwistle G. and Subrahmanyam P.A., Kluwer, 1988.","DOI":"10.1007\/978-1-4613-2007-4_1"},{"key":"35_CR8","doi-asserted-by":"crossref","unstructured":"J.Joyce: Formal Verification and Implementation of a Microprocessor, VLSI Specification, Verification and Synthesis, Eds. Birwistle G. and Subrahmanyam P.A., Kluwer, 1988.","DOI":"10.1007\/978-1-4613-2007-4_4"},{"key":"35_CR9","doi-asserted-by":"crossref","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill: Sequential Circuit Verification Using Symbolic Model Checking; Proc. 27th Design Automation Conference (DAC 90), 1990, pp. 46\u201351.","DOI":"10.1145\/123186.123223"},{"key":"35_CR10","doi-asserted-by":"crossref","unstructured":"O. Coudert, C. Berthet, J.C. Madre: Verification of Synchronous Sequential Machines Based on Symbolic Execution; Proc. Workshop on Automatic Verification Methods for Finite State Systems, Grenoble, June 1989.","DOI":"10.1007\/3-540-52148-8_30"},{"key":"35_CR11","doi-asserted-by":"crossref","unstructured":"T. Kropf, H.-J. Wunderlich: A Common Approach to Hardware Verification and Test Generation Based on Temporal Logic; Proc. International Test Conference (ITC 91), Nashville, 1991.","DOI":"10.1109\/TEST.1991.519494"},{"key":"35_CR12","unstructured":"Abstract Hardware Limited: LAMBDA \u2014 Logic and Mathematics behind Design Automation; User and Reference Manuals, Version 3.1, 1990."},{"key":"35_CR13","volume-title":"Proc. VLSI '91","author":"K. Schneider","year":"1991","unstructured":"K. Schneider, R. Kumar, T. Kropf: Structuring Hardware Proofs: First Steps towards Automation in a Higher-Order Environment; Proc. VLSI '91, Edinburgh, P.B. Denyer, A. Halaas (Eds.), North-Holland, 1991."},{"key":"35_CR14","doi-asserted-by":"crossref","unstructured":"M. Gordon: A Proof Generating System for Higher-Order Logic; VLSI Specification, Verification and Synthesis, Eds. Birwistle G. and Subrahmanyam P.A., Kluwer, 1988.","DOI":"10.1007\/978-1-4613-2007-4_3"},{"key":"35_CR15","doi-asserted-by":"crossref","unstructured":"M. Fitting: First-Order Logic and Automated Theorem Proving; Springer Verlag, 1990.","DOI":"10.1007\/978-1-4684-0357-2"},{"key":"35_CR16","volume-title":"Harper & Row Computer Science and Technology Series No. 5","author":"J. H. Gallier","year":"1986","unstructured":"J.H. Gallier: Logic for Computer Science: Foundations of Automatic Theorem Proving; Harper & Row Computer Science and Technology Series No. 5, Harper & Row Publishers, New York, 1986."},{"key":"35_CR17","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1007\/BF00244513","volume":"4","author":"E. Oppacher","year":"1988","unstructured":"Oppacher E., Suen: HARP: A Tableaux-based Theorem Prover, Journal of Automated Reasoning; Vol. 4, 1988, pp. 69\u2013100.","journal-title":"Journal of Automated Reasoning"},{"key":"35_CR18","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1145\/321250.321253","volume":"12","author":"J. A. Robinson","year":"1965","unstructured":"J.A. Robinson: A Machine-oriented logic based on the resolution principle; Journal of the ACM, Vol. 12, pp. 23\u201341, 1965.","journal-title":"Journal of the ACM"},{"key":"35_CR19","unstructured":"K. Schneider: Ein Sequenzenkalk\u00fcl f\u00fcr die Hardware-Verifikation in HOL; Diploma Thesis, Institute of Computer Design and Fault-Tolerance, University of Karlsruhe, 1991."},{"key":"35_CR20","unstructured":"Schneider K., Kumar R., Kropf T.: Technical Report, Dept. of Comp. Sc. Univ. of Karlsruhe, 1991, (to appear)."},{"key":"35_CR21","volume-title":"Proc. 1991 International Tutorial and Workshop on the HOL Theorem Proving System and its Applications","author":"R. Kumar","year":"1991","unstructured":"R. Kumar, T. Kropf, K. Schneider: Integrating a First-Order Automatic Prover in the HOL Environment; Proc. 1991 International Tutorial and Workshop on the HOL Theorem Proving System and its Applications, Davis, California, Aug. 1991."},{"key":"35_CR22","unstructured":"D. Kalish, R. Montague: Logic: Techniques of Formal Reasoning; World, Harcourt & Brace, 1964."},{"key":"35_CR23","doi-asserted-by":"crossref","first-page":"191","DOI":"10.1007\/BF02432151","volume":"2","author":"F. J. Pelletier","year":"1986","unstructured":"F.J. Pelletier: Seventy-Five Problems for Testing Automatic Theorem Provers; Journal of Automated Reasoning, Vol. 2, pp. 191\u2013216, 1986.","journal-title":"Journal of Automated Reasoning"},{"key":"35_CR24","unstructured":"Proceedings of the Third HOL Users Meeting; Aarhus University, Oct. 1990."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-55179-4_35.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:58:00Z","timestamp":1605646680000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-55179-4_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992]]},"ISBN":["9783540551799","9783540467632"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/3-540-55179-4_35","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1992]]}}}