{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:10:27Z","timestamp":1725664227850},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540590477"},{"type":"electronic","value":"9783540491774"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-59047-1_43","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:01:42Z","timestamp":1330275702000},"page":"72-91","source":"Crossref","is-referenced-by-count":5,"title":["An automatic generalization method for the inductive proof of replicated and parallel architectures"],"prefix":"10.1007","author":[{"given":"Laurence","family":"Pierre","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"key":"5_CR1","unstructured":"P. ASHAR, A. GHOSH, S. DEVADAS, A. NEWTON: \u201cCombinational and sequential logic verification using general binary decision diagrams\u201d. Proc. Int. Workshop on Logic Synthesis, Research Triangle Park (NC), May 1991."},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"R. AUBIN: \u201cMechanizing structural induction-Part II: Strategies\u201d. Theoretical Computer Science 9. North-Holland, 1979. pp. 347\u2013362.","DOI":"10.1016\/0304-3975(79)90035-5"},{"key":"5_CR3","unstructured":"R.S. BOYER, J. S. MOORE: \u201cA Computational Logic\u201d. ACM Monograph Series. Academic Press, Ins. 1979."},{"key":"5_CR4","unstructured":"R.S. BOYER, J. S. MOORE: \u201cA Computational Logic Handbook\u201d. Perspectives in Computing, Vol. 23. Academic Press, Inc. 1988."},{"key":"5_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\u22182, June 1992.","DOI":"10.1109\/54.143145"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"R.E. BRYANT: \u201cGraph-based Algorithms for Boolean Function Manipulation\u201d. IEEE Transactions on Computers, Vol. C-35, n\u22188, August 1986.","DOI":"10.1109\/TC.1986.1676819"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"R.E. BRYANT: \u201cOn the Complexity of VLSI Implementations and Graph Representations of Boolean Functions with Application to Integer Multiplication\u201d. IEEE Transactions on Computers, Vol. 40, n\u22182, February 1991.","DOI":"10.1109\/12.73590"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"J.R. BURCH: \u201cUsing BDDs to verify multipliers\u201d. Proc. DAC'91, San Francisco (CA), June 1991.","DOI":"10.1145\/127601.127703"},{"key":"5_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\u22187. July 1988.","DOI":"10.1109\/2.65"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"M. FUJITA, H. FUJISAWA, N. KAWATO: \u201cEvaluation and Improvements of Boolean Comparison Method based on Binary Decision Diagrams\u201d. Proc. Int. Conference on Computer-Aided Design ICCAD'88, 1988.","DOI":"10.1109\/ICCAD.1988.122450"},{"volume-title":"Technical Report n\u221847","year":"1986","author":"W.A. Hunt","key":"5_CR11","unstructured":"W.A. HUNT: \u201cFM8501: A verified microprocessor\u201d. Institute for Computing Science, University of Texas, Austin (USA). Technical Report n\u221847. February 1986."},{"volume-title":"Computer arithmetic: principles, architecture and design","year":"1979","author":"K. Hwang","key":"5_CR12","unstructured":"K. HWANG: \u201cComputer arithmetic: principles, architecture and design\u201d, John Wiley & sons Inc., New-York, 1979."},{"key":"5_CR13","unstructured":"IEEE Standard VHDL Language Reference Manual, IEEE. 1988."},{"key":"5_CR14","unstructured":"T. KROPF: \u201cBenchmark-Circuits for Hardware Verification, 2nd TPCD Conference\u201d. 2nd Conference on Theorem Proving in Circuit Design, Bad Herrenalb (Germany), 1994."},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"J.S. MOORE: \u201cIntroducing Iteration into the Pure Lisp Theorem Prover\u201d. IEEE Transactions on Software Engineering, Vol. SE-1, n\u22183. September 1975.","DOI":"10.1109\/TSE.1975.6312857"},{"key":"5_CR16","doi-asserted-by":"crossref","first-page":"2","DOI":"10.1016\/0004-3702(75)90008-9","volume":"6","author":"Z. Manna","year":"1975","unstructured":"Z. MANNA, R. WALDINGER: \u201cKnowledge and Reasoning in Program Synthesis\u201d. Artificial Intelligence Journal. Vol. 6, 2. 1975.","journal-title":"Artificial Intelligence Journal."},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"S. MALIK, A.R. WANG, R.K. BRAYTON, A. SANGIOVANNI-VINCENTELLI: \u201cLogic Verification using Binary Decision Diagrams in a Logic Synthesis Environment\u201d. Proc. Int. Conference on Computer-Aided Design ICCAD'88, 1988.","DOI":"10.1109\/ICCAD.1988.122451"},{"key":"5_CR18","unstructured":"L. PIERRE: \u201cThe Formal Proof of the Min-Max sequential benchmark described in CASCADE using the Boyer-Moore Theorem Prover\u201d. Proc. IFIP WG 10.2 Int. Workshop Nov. 1989. In \u201cFormal VLSI Correctness Verification\u201d, L. Claesen ed., North Holland, 1990."},{"key":"5_CR19","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 (Fl). 9\u201311 January 1991."},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"L. PIERRE: \u201cVHDL Description and Formal Verification of Systolic Multipliers\u201d. In \u201cCHDL and their Applications\u201d, D. Agnew, L. Claesen & R. Camposano Eds., North Holland, 1993.","DOI":"10.1016\/B978-0-444-81641-2.50023-X"},{"key":"5_CR21","unstructured":"H. SIMONIS: \u201cFormal verification of multipliers\u201d. Proc. IFIP WG 10.2 Int. Workshop Nov. 1989. In \u201cFormal VLSI Correctness Verification\u201d, L. Claesen ed., North Holland, 1990."},{"key":"5_CR22","unstructured":"D. VERKEST, L. CLAESEN, H. DE MAN: \u201cSpecial Benchmark Session on Formal System Design\u201d. Proc. IFIP WG 10.2 Int. Workshop Nov. 1989. In \u201cFormal VLSI Correctness Verification\u201d, L. Claesen ed., North Holland, 1990."},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"F. WAGNER: \u201cPrevail-DM: a framework-based environment for formal hardware verification\u201d. In \u201cCHDL and their Applications\u201d, D. Agnew, L. Claesen & R. Camposano Eds., North Holland, 1993.","DOI":"10.1016\/B978-0-444-81641-2.50011-3"}],"container-title":["Lecture Notes in Computer Science","Theorem Provers in Circuit Design"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-59047-1_43.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:25:22Z","timestamp":1605648322000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-59047-1_43"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540590477","9783540491774"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/3-540-59047-1_43","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}