{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:13:19Z","timestamp":1725664399703},"publisher-location":"Berlin, Heidelberg","reference-count":33,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540603856"},{"type":"electronic","value":"9783540455165"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-60385-9_3","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T18:23:43Z","timestamp":1330280623000},"page":"35-55","source":"Crossref","is-referenced-by-count":3,"title":["Describing and verifying synchronous circuits with the Boyer-Moore theorem prover"],"prefix":"10.1007","author":[{"given":"Laurence","family":"Pierre","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,2]]},"reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"R.BURSTALL, J.DARLINGTON: \u201cA transformation system for developing recursive programs\u201d. Journal of the ACM. Vol. 24, 1. January 1977.","DOI":"10.1145\/321992.321996"},{"key":"3_CR2","doi-asserted-by":"crossref","unstructured":"J.M.BERG\u00e9, A.FONKOUA, S.MAGINOT, J.ROUILLARD: \u201cVHDL'92: The New Features of the VHDL Hardware Description Language\u201d. Kluwer Academic Pub., 1993.","DOI":"10.1007\/978-1-4615-3246-0"},{"key":"3_CR3","doi-asserted-by":"crossref","unstructured":"F.P.BURNS, D.J.KINNIMENT, A.M.KOELMANS: \u201cCorrect interactive transformational synthesis of DSP hardware\u201d. Proc. European Design Automation Conference. Amsterdam (The Netherlands). 25\u201328 February 1991.","DOI":"10.1109\/EDAC.1991.206350"},{"key":"3_CR4","unstructured":"R.S.BOYER, J S.MOORE: \u201cA Computational Logic Handbook\u201d. Perspectives in Computing, Vol. 23. Academic Press, Inc. 1988."},{"key":"3_CR5","doi-asserted-by":"crossref","unstructured":"D.BORRIONE, L.PIERRE, A.SALEM: \u201cFormal Verification of VHDL Descriptions in the PREVAIL Environment\u201d. IEEE Design&Test Magazine, Vol. 9, n\u21342. June 1992.","DOI":"10.1109\/54.143145"},{"key":"3_CR6","unstructured":"A.BRONSTEIN: \u201cString-Functional Semantics and the Boyer-Moore Mechanization for the Formal Verification of Synchronous Circuits\u201d. PhD Thesis, Stanford University, Report n\u2134 STAN-CS-89-1293. December 1989."},{"key":"3_CR7","unstructured":"A.BRONSTEIN, C.L.TALCOTT: \u201cFormal Verification of Pipelines based on String-Functional Semantics\u201d. Proc. IFIP WG 10.2 Int. Workshop Nov. 1989. In \u201cFormal VLSI Correctness Verification\u201d, L.Claesen Ed., North Holland, 1990."},{"key":"3_CR8","unstructured":"R.CAMPOSANO: \u201cStructural Synthesis: Some References\u201d. Advanced Summer Course on \u201cLogic Synthesis and Silicon Compilation for VLSI Design\u201d. L'Aquila (Italy). 13\u201318 July 1987."},{"key":"3_CR9","doi-asserted-by":"crossref","unstructured":"P.CAMURATI, P.PRINETTO: \u201cFormal Verification of Hardware Correctness: Introduction and Survey of Current Research\u201d. IEEE Computer, Vol.21, n\u21347. July 1988.","DOI":"10.1109\/2.65"},{"key":"3_CR10","unstructured":"S.COUPET-GRIMAL, L.PIERRE: \u201cRecursive Models for Synchronous Sequential Devices\u201d. Research Report IMAG\/ARTEMIS n\u2134 855-I, Grenoble (France). July 1991."},{"key":"3_CR11","unstructured":"D.DIETMEYER: \u201cLogic Design of Digital Systems\u201d. Allyn and Bacon. 1978."},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"M.GORDON: \u201cThe denotational semantics of sequential machines\u201d. Information Processing Letters, Vol.10, n\u21341. February 1980.","DOI":"10.1016\/0020-0190(80)90111-8"},{"key":"3_CR13","volume-title":"LCF-LSM\u201d. Technical Report n\u213441","author":"M. Gordon","year":"1984","unstructured":"M.GORDON: \u201cLCF-LSM\u201d. Technical Report n\u213441. Univ. of Cambridge (UK). 1984."},{"key":"3_CR14","volume-title":"Technical Report n\u213468","author":"M. Gordon","year":"1985","unstructured":"M.GORDON: \u201cHOL: a machine-oriented formulation of higher order logic\u201d. Technical Report n\u213468. University of Cambridge (UK). May 1985."},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"A.GUPTA: \u201cFormal Hardware Verification Methods: a Survey\u201d. Formal Methods in System Design, Vol.1, 1992.","DOI":"10.1007\/BF00121125"},{"key":"3_CR16","unstructured":"S.M.GERMAN, Y.WANG: \u201cFormal Verification of Parameterized Hardware Designs\u201d. Proc. IEEE Int. Conf. on Computer Design: VLSI in Computers, October 1985."},{"key":"3_CR17","volume-title":"The Verification of a Bit-slice ALU","author":"W.A. Hunt","year":"1989","unstructured":"W.A.HUNT, B.C.BROCK: \u201cThe Verification of a Bit-slice ALU\u201d. Workshop on Hardware Specification, Verification and Synthesis: Mathematical Aspects. Cornell University, Ithaca, NY (USA). 5\u20137 July 1989."},{"key":"3_CR18","doi-asserted-by":"crossref","unstructured":"P.HARRISON, H.KHOSHNEVISAN: \u201cA new approach to recursion removal\u201d. Theoretical Computer Science 93, 1992.","DOI":"10.1016\/0304-3975(92)90213-Y"},{"key":"3_CR19","doi-asserted-by":"crossref","unstructured":"G.HUET, B.LANG: \u201cProving and Applying Program Transformations Expressed with Second-Order Patterns\u201d. Acta Informatica 11. 1978.","DOI":"10.1007\/BF00264598"},{"key":"3_CR20","volume-title":"Technical Report n\u213447","author":"W.A. Hunt","year":"1986","unstructured":"W.A.HUNT: \u201cFM8501: A verified microprocessor\u201d. Institute for Computing Science, University of Texas, Austin (USA). Technical Report n\u213447. February 1986."},{"key":"3_CR21","unstructured":"IEEE Standard VHDL Language Reference Manual, IEEE. 1988."},{"key":"3_CR22","volume-title":"Synthesis of Digital Designs from Recursion Equations","author":"S.D. Johnson","year":"1984","unstructured":"S.D.JOHNSON: \u201cSynthesis of Digital Designs from Recursion Equations\u201d. The MIT Press, Cambridge. 1984."},{"key":"3_CR23","unstructured":"S.D.JOHNSON: \u201cDigital Design in a Functional Calculus\u201d. In G.J.Milne and P.A.Subrahmanyam Eds., Proc. of the Workshop on Formal Aspects of VLSI Design. Elsevier Science Publishers, 1986."},{"key":"3_CR24","unstructured":"G.KAHN: \u201cThe Semantics of a Simple Language for Parallel Programming\u201d. Proc. IFIP Congress 74. Amsterdam (The Netherlands). 1974."},{"key":"3_CR25","unstructured":"M.KAUFMANN, P.PECCHIARI: \u201cInteraction with the Boyer-Moore Theorem Prover: a Tutorial Study using the Arithmetic-Geometric Mean Theorem\u201d, Technical Report n\u2134100, Computational Logic Inc., August 1994."},{"key":"3_CR26","volume-title":"Hardware Description with Recursion Equations","author":"J.T.O' Donnell","year":"1987","unstructured":"J.T.O'DONNELL: \u201cHardware Description with Recursion Equations\u201d. Proc. Int. Conf. on CHDL'87, Amsterdam (The Netherlands). M.Barbacci and C.Koomen Eds., Elsevier Science Publishers, 1987."},{"key":"3_CR27","unstructured":"L.PIERRE: \u201cOne Aspect of Mechanizing Formal Proof of Hardware: the Generalization of Partial Specifications\u201d. Proc. ACM International Workshop on Formal Methods in VLSI Design. Miami (USA). January 1991."},{"key":"3_CR28","volume-title":"CHDL and their Applications","author":"L. Pierre","year":"1991","unstructured":"L.PIERRE: \u201cFrom a HDL Description to Formal Proof Systems: Principles and Mechanization\u201d. Proc. 10th Int. Symposium CHDL'91. Marseille (France), April 1991. In \u201cCHDL and their Applications\u201d, D.Borrione & R.Waxman ed., North Holland, 1991."},{"key":"3_CR29","doi-asserted-by":"crossref","unstructured":"L.PIERRE: \u201cAn automatic generalization method for the inductive proof of replicated and parallel architectures\u201d. Proc. International Conference on Theorem Provers in Circuit Design. Bad Herrenalb (Germany), September 1994.","DOI":"10.1007\/3-540-59047-1_43"},{"key":"3_CR30","doi-asserted-by":"crossref","unstructured":"D.M.RUSSINOFF: \u201cA Mechanical Proof of Quadratic Reciprocity\u201d. Journal of Automated Reasoning, Vol.8, n\u21341, 1992.","DOI":"10.1007\/BF00263446"},{"key":"3_CR31","volume-title":"Technical Report n\u213445","author":"N. Shankar","year":"1985","unstructured":"N.SHANKAR: \u201cA mechanical proof of the Church-Rosser theorem\u201d. Institute for Computing Science, University of Texas, Austin. Technical Report n\u213445. March 1985."},{"key":"3_CR32","unstructured":"D.VERKEST, J.VANDENBERGH, L.CLAESEN, H.DE MAN: \u201cA description methodology for parameterized modules in the Boyer-Moore logic\u201d. In \u201cTheorem provers in circuit design\u201d, V.Stavridou, T.Melham & R.Boute ed., North Holland, 1992."},{"key":"3_CR33","doi-asserted-by":"crossref","unstructured":"Y.YU: \u201cComputer Proofs in Group Theory\u201d. Journal of Automated Reasoning, Vol.6, n\u21343, 1990.","DOI":"10.1007\/BF00244488"}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-60385-9_3.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T20:58:56Z","timestamp":1605646736000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-60385-9_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540603856","9783540455165"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/3-540-60385-9_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}