{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,4,5]],"date-time":"2022-04-05T10:27:14Z","timestamp":1649154434941},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[1993,2,1]],"date-time":"1993-02-01T00:00:00Z","timestamp":728524800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[1993,2]]},"DOI":"10.1007\/bf01383943","type":"journal-article","created":{"date-parts":[[2005,4,1]],"date-time":"2005-04-01T21:05:31Z","timestamp":1112389531000},"page":"45-72","source":"Crossref","is-referenced-by-count":1,"title":["On the comparison of HOL and Boyer-Moore for formal hardware verification"],"prefix":"10.1007","volume":"2","author":[{"given":"C. M.","family":"Angelo","sequence":"first","affiliation":[]},{"given":"D.","family":"Verkest","sequence":"additional","affiliation":[]},{"given":"L.","family":"Claesen","sequence":"additional","affiliation":[]},{"given":"D. H.","family":"De Man","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"6","key":"CR1","first-page":"73","volume":"3","author":"H. Man De","year":"1986","unstructured":"H. De Man, J. Rabaey, P. Six, and L. Claesen. Cathedral-II: a silicon compiler for digital signal processing.IEEE Design & Test of Computers, 3(6):73?85 (December 1986)","journal-title":"IEEE Design & Test of Computers"},{"key":"CR2","unstructured":"S. M. German, and Y. Wang. Formal verification of parameterized hardware designs.Proceedings IEEE International Conference on Computer Design: VLSI in Computers, ICCD-85, October 1985, pp. 549?552."},{"key":"CR3","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1007\/978-1-4613-2007-4_3","volume-title":"VLSI Specification, Verification and Synthesis","author":"M. Gordon","year":"1988","unstructured":"M. Gordon. HOL: a proof generating system for higher-order logic.VLSI Specification, Verification and Synthesis, G. Birtwistle and P.A. Subrahmanyam (eds.). Academic Press, Boston, 1988, pp. 73?127."},{"key":"CR4","volume-title":"A Computational Logic Handbook","author":"R.S. Boyer","year":"1988","unstructured":"R.S. Boyer and J.S. Moore.A Computational Logic Handbook. Academic Press, New York, 1988."},{"key":"CR5","first-page":"150","volume-title":"Introduction to VLSI Systems","author":"C. Mead","year":"1980","unstructured":"C. Mead, and L. Conway.Introduction to VLSI Systems. Addison-Wesley, Reading, MA, 1980, pp. 150?154."},{"key":"CR6","doi-asserted-by":"crossref","unstructured":"D. Verkest, L. Claesen, and H. De Man. Correctness proofs of parameterized hardware modules in the Cathedral-II synthesis environment.European Design Automation Conference EDAC 90. IEEE Computer Society Press, pp. 62?66.","DOI":"10.1109\/EDAC.1990.136621"},{"key":"CR7","first-page":"43","volume-title":"CHDL'91, IFIP, Tenth International Symposium on Computer Hardware Description Languages and their Applications","author":"C.M. Angelo","year":"1991","unstructured":"C.M. Angelo, L. Claesen, and H. De Man. A methodology for proving correctness of parameterized hardware modules in HOL.CHDL'91, IFIP, Tenth International Symposium on Computer Hardware Description Languages and their Applications, D. Borrione and R. Waxman (eds.). Elsevier\/North Holland, April, 1991, Marseille, France, pp. 43?62."},{"key":"CR8","doi-asserted-by":"crossref","unstructured":"V. Stavridou, H. Barringer, and D.A. Edwards. Formal specification and verification of hardware: a comparative case study.25th ACM\/IEEE Design Automation Conference, 1988, pp. 197?203.","DOI":"10.1109\/DAC.1988.14758"},{"key":"CR9","unstructured":"B. Levy. An overview of hardware verification using the state delta verification system.1991 International Workshop on Formal Methods in VLSI Design, Jan 9?11, 1991, Miami, FL."},{"issue":"9","key":"CR10","doi-asserted-by":"crossref","first-page":"8","DOI":"10.1109\/2.58215","volume":"23","author":"J.M. Wing","year":"1990","unstructured":"J.M. Wing. A specifier's introduction to formal methods.IEEE Computer magazine, 23(9):8?24 (September 1990).","journal-title":"IEEE Computer magazine"},{"key":"CR11","first-page":"153","volume-title":"Formal Aspects of VLSI Design","author":"M. Gordon","year":"1986","unstructured":"M. Gordon. Why higher-order logic is a good formalism for specifying and verifying hardware.Formal Aspects of VLSI Design G. Milne and P.A. Subrahmanyam, (eds.). North Holland, Amsterdam, 1986, pp. 153?178."},{"key":"CR12","first-page":"43","volume-title":"From HDL Descriptions to Guaranteed Correct Circuit Designs","author":"A.J. Camilleri","year":"1987","unstructured":"A.J. Camilleri, M. Gordon, and T. Melham. Hardware verification using higher-order logic.From HDL Descriptions to Guaranteed Correct Circuit Designs. D. Borrione (ed.). Elsevier Science Publishers B.V., North Holland, IFIP 1987, pp. 43?67."},{"key":"CR13","volume-title":"The ML Handbook","author":"G. Cousineau","year":"1986","unstructured":"G. Cousineau, M. Gordon, G. Huet, R. Milner, L. Paulson, and C. Wadsworth,The ML Handbook. INRIA, France 1986."},{"key":"CR14","volume-title":"A Computational Logic","author":"R.S. Boyer","year":"1979","unstructured":"R.S. Boyer, and J.S. Moore,A Computational Logic. Academic Press, New York, 1979."},{"key":"CR15","unstructured":"J.J. Joyce.Multi-Level Verification of Microprocessor Based Systems. Ph.D. thesis, Computer Laboratory, Cambridge University, December 1989."},{"key":"CR16","unstructured":"P.J. Windley, Abstract hardware.Proceedings of the ACM\/SIGDA International Workshop in Formal Methods in VLSI Design, Miami, FL. January 1991."},{"key":"CR17","unstructured":"S-K. Chin. Verified synthesis functions for negabinary arithmetic hardware.IMEC-IFIP International Workshop on Applied Formal Methods for Correct VLSI Design I, Belgium, November 1989, L. Claesen, (ed.). Elsevier Science Publishers, Amsterdam pp. 226?235."},{"key":"CR18","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1016\/0743-1066(87)90022-7","volume":"4","author":"W.F. Clocksin","year":"1987","unstructured":"W.F. Clocksin. Logic programming and digital circuit analysis.The Journal of Logic Programming, 4:59?82 (1987).","journal-title":"The Journal of Logic Programming"},{"key":"CR19","first-page":"147","volume-title":"Design Methodologies for VLSI and Computer Architecture","author":"A.J. Camilleri","year":"1989","unstructured":"A.J. Camilleri. Simulation as an aid to verification using the HOL theorem prover.Design Methodologies for VLSI and Computer Architecture, D.A. Edwards, (ed.). Elsevier Science Publishers B.V., North-Holland, IFIP, 1989 pp. 147?168"},{"key":"CR20","doi-asserted-by":"crossref","first-page":"267","DOI":"10.1007\/978-1-4613-2007-4_9","volume-title":"VLSI Specification, Verification and Synthesis: Proceedings of the Hardware Verification Workshop Calgary, Canada, 12?16 January 1987","author":"T.F. Melham","year":"1988","unstructured":"T.F. Melham. Abstraction mechanisms for hardware verification.VLSI Specification, Verification and Synthesis: Proceedings of the Hardware Verification Workshop Calgary, Canada, 12?16 January 1987, G. Birtwistle and P.A. Subrahmanyam (ed.). Kluwer Academic Publishers, Boston, 1988, pp. 267?291."},{"key":"CR21","first-page":"379","volume-title":"Formal VLSI Correctness Verification, VLSI Design Methods II","author":"J. Herbert","year":"1990","unstructured":"J. Herbert. Formal reasoning about the timing and function of basic memory devices.Formal VLSI Correctness Verification, VLSI Design Methods II, L. Claesen, (ed.). Elsevier Science Publishers B.V., North-Holland, IFIP 1990, pp. 379?398."},{"key":"CR22","volume-title":"FM8501, a verified microprocessor","author":"W.A. Hunt","year":"1985","unstructured":"W.A. Hunt.FM8501, a verified microprocessor Ph.D. thesis, Department of Computer Sciences, University of Texas at Austin, TX, 1985."},{"key":"CR23","first-page":"309","volume-title":"Formal VLSI Correctness Verification, VLSI Design Methods II","author":"L. Pierre","year":"1990","unstructured":"L. Pierre. The formal proof of sequential circuits described in CASCADE using the Boyer-Moore theorem prover.Formal VLSI Correctness Verification, VLSI Design Methods II, L. Claesen, (ed.). Elsevier Science Publishes, North Holland, 1990, pp. 309?328."},{"key":"CR24","doi-asserted-by":"crossref","first-page":"341","DOI":"10.1007\/978-1-4612-3658-0_9","volume-title":"Current Trends in Hardware Verification and Automated Theorem Proving","author":"T.F. Melham","year":"1989","unstructured":"T.F. Melham. Automating recursive type definitions in higher order logic.Current Trends in Hardware Verification and Automated Theorem Proving, G. Birtwistle and P.A. Subrahmanyam, (eds.). Springer-Verlag, New York, 1989, pp. 341?386."},{"key":"CR25","unstructured":"T.F. Melham. Using recursive types to reason about hardware in higher order logic.The Fusion of Hardware Design and Verification: Proceedings of the IFIP WG 10.2 Working Conference, Glasgow, July 1988, G.J. Milne (ed.). North-Holland, Amsterdam, pp. 27?50."},{"key":"CR26","unstructured":"B.C. Brock and W.A. Hunt, Jr. The formalization of a simple hardware description language.IMEC-IFIP International Workshop on Applied Formal Methods for Correct VLSI Design II, Belgium, November 1989, L. Claesen, (ed.). Elsevier Science Publishers, Amsterdam, pp. 778?793."},{"key":"CR27","first-page":"285","volume-title":"Formal Methods for VLSI Design","author":"B.C. Brock","year":"1990","unstructured":"B.C. Brock, and W.A. Hunt, Jr. A formal introduction, to a, simple HDL.Formal Methods for VLSI Design, IFIP, 1990, J. Staunstrup (ed.) Elsevier Science Publishers, Amsterdam, pp. 285?329."},{"key":"CR28","unstructured":"R. Boulton, M. Gordon, J. Herbert, and J. Van Tassel. The HOL verification of ELLA designs.Proceedings of the International Workshop on Formal Methods in VLSI Design, Miami, 1991."},{"key":"CR29","unstructured":"J.D. Morison, N.E. Peeling, and T.L. Thorp. ELLA: hardware description or specification?Proceedings of the IEEE International Conference, CAD-84, Santa Clara, CA, November 1984."},{"key":"CR30","volume-title":"IEEE Standard VHDL Language Reference Manual","author":"Institute of Electrical and Electronics Engineers","year":"1988","unstructured":"Institute of Electrical and Electronics Engineers,IEEE Standard VHDL Language Reference Manual. IEEE Press, New York, 1988."},{"key":"CR31","unstructured":"P.N. Hilfinger, Silage, a high-level language and silicon compiler for digital signal processing.Proceedings IEEE CICC-85, Portland, OR, May 1985, pp. 213?216."},{"key":"CR32","unstructured":"A.D. Gordon. A mechanised definition of silage in HOL. Internal report, Computer Laboratory, University of Cambridge, February 1992."},{"key":"CR33","volume-title":"Proceedings ofHOL'92 International Workshop on Higher Order Logic Theorem Proving and Its Applications","author":"C.M. Angelo","year":"1992","unstructured":"C.M. Angelo, L. Claesen, and H. De Man The formal semantics definition of a multi-rate DSP specification language in HOL. To appear in the Proceedings ofHOL'92 International Workshop on Higher Order Logic Theorem Proving and Its Applications L. Claesen and M. Gordon (eds.). Elsevier\/North Holland, Leuven, Belgium, September 1992"},{"key":"CR34","series-title":"Technical Report","volume-title":"A user's manual for an interactive enhancement to the Boyer-Moore theorem prover","author":"M. Kaufmann","year":"1988","unstructured":"M. Kaufmann. A user's manual for an interactive enhancement to the Boyer-Moore theorem prover.Technical Report, 19, Computational Logic Inc., Austin, TX, May 1988."},{"key":"CR35","unstructured":"M. Kaufmann. DEFN-SK: an extension of the Boyer-Moore theorem prover to handle first-order quantifiers.Technical Report 43, Computational Logic Inc., Austin, TX, May 1989. To appear in theJournal of Automated Reasoning."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01383943.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01383943\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01383943","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,2]],"date-time":"2019-05-02T12:04:47Z","timestamp":1556798687000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01383943"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993,2]]},"references-count":35,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1993,2]]}},"alternative-id":["BF01383943"],"URL":"https:\/\/doi.org\/10.1007\/bf01383943","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993,2]]}}}