{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:47:58Z","timestamp":1725551278384},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540665595"},{"type":"electronic","value":"9783540481539"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48153-2_15","type":"book-chapter","created":{"date-parts":[[2010,3,29]],"date-time":"2010-03-29T17:13:28Z","timestamp":1269882808000},"page":"187-202","source":"Crossref","is-referenced-by-count":4,"title":["Formal Synthesis at the Algorithmic Level"],"prefix":"10.1007","author":[{"given":"Christian","family":"Blumenr\u00f6hr","sequence":"first","affiliation":[]},{"given":"Viktor","family":"Sabelfeld","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,6,3]]},"reference":[{"issue":"2\/3","key":"15_CR1","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/BF00121125","volume":"1","author":"A. Gupta","year":"1992","unstructured":"A. Gupta. Formal hardware verification methods: A survey. Formal Methods in System Design, 1(2\/3):151\u2013238, 1992.","journal-title":"Formal Methods in System Design"},{"key":"15_CR2","unstructured":"P. Middelhoek. Transformational Design. PhD thesis, Univ. Twente,NL, 1997."},{"key":"15_CR3","doi-asserted-by":"crossref","unstructured":"M. McFarland. Formal analysis of correctness of behavioral transformations. Formal Methods in System Design, 2(3), 1993.","DOI":"10.1007\/BF01384133"},{"issue":"2","key":"15_CR4","doi-asserted-by":"crossref","first-page":"150","DOI":"10.1109\/43.259939","volume":"13","author":"Z. Peng","year":"1994","unstructured":"Z. Peng, K. Kuchcinski. Automated transformation of algorithms into register-transfer implementations. IEEE Transactions on CAD, 13(2):150\u2013166, 1994.","journal-title":"IEEE Transactions on CAD"},{"key":"15_CR5","series-title":"Lect Notes Comput Sci","first-page":"106","volume-title":"Hardware Specification, Verification and Synthesis: Mathematical Aspects","author":"R. Camposano","year":"1989","unstructured":"R. Camposano. Behavior-preserving transformations for high-level synthesis. In Hardware Specification, Verification and Synthesis: Mathematical Aspects, number 408 in LNCS, pp. 106\u2013128, Ithaca, New York, 1989. Springer."},{"key":"15_CR6","unstructured":"S. D. Johnson, B. Bose. DDD: A system for mechanized digital design derivation. In Int. Workshop on Formal Methods in VLSI Design, Miami, Florida, 1991. Available via \u201c ftp:\/\/ftp.cs.indiana.edu\/pub\/techreports\/TR323.ps.Z \u201d (rev. 1997)."},{"key":"15_CR7","unstructured":"M. J. C. Gordon, T. F. Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993."},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"R. Sharp, O. Rasmussen. The T-Ruby design system. In IFIP Conference on Hardware Description Languages and their Applications, pp. 587\u2013596, 1995.","DOI":"10.1109\/ASPDAC.1995.486374"},{"key":"15_CR9","unstructured":"E. M. Mayger, M. P. Fourman. Integration of formal methods with system design. In Int. Conf. on VLSI,pp. 59\u201370, Edinburgh,Scotland, 1991. North-Holland."},{"key":"15_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"294","DOI":"10.1007\/BFb0031817","volume-title":"FMCAD\u201996","author":"R. Kumar","year":"1996","unstructured":"R. Kumar et al. Formal synthesis in circuit design-A classification and survey. In FMCAD\u201996, number 1166 in LNCS, pp. 294\u2013309, Palo Alto, CA, 1996. Springer."},{"key":"15_CR11","first-page":"532","volume":"2","author":"F. K. Hanna","year":"1989","unstructured":"F. K. Hanna et al. Formal synthesis of digital systems. In Applied Formal Methods For Correct VLSI Design, volume 2, pp. 532\u2013548. Elsevier, 1989.","journal-title":"Applied Formal Methods For Correct VLSI Design"},{"issue":"2","key":"15_CR12","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1093\/comjnl\/38.2.101","volume":"38","author":"M. Larsson","year":"1995","unstructured":"M. Larsson. An engineering approach to formal digital system design. The Computer Journal, 38( 2):101\u2013110, 1995.","journal-title":"The Computer Journal"},{"key":"15_CR13","doi-asserted-by":"crossref","unstructured":"D. Gajski et al. High-Level Synthesis, Introduction to Chip and System Design. Kluwer, 1992.","DOI":"10.1007\/978-1-4615-3636-9_1"},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"H.P. Barendregt. Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics, chapter 7: Functional Programming and Lambda Calculus, pp. 321\u2013364. Elsevier, 1992.","DOI":"10.1016\/B978-0-444-88074-1.50012-3"},{"key":"15_CR15","unstructured":"A. Aho et al. Compilers: Principles, Techniques and Tools. Addison Wesley, 1986."},{"issue":"6","key":"15_CR16","doi-asserted-by":"crossref","first-page":"661","DOI":"10.1109\/43.31522","volume":"8","author":"P. G. Paulin","year":"1989","unstructured":"P. G. Paulin, J. P. Knight. Force-directed scheduling for the behavioral synthesis of ASIC\u2019s. IEEE Transactions on CAD, 8(6):661\u2013679, 1989.","journal-title":"IEEE Transactions on CAD"},{"key":"15_CR17","unstructured":"C. Blumenr\u00f6hr. A formal approach to specify and synthesize at the system level. In GI Workshop Modellierung und Verifikation von Systemen, pp. 11\u201320,Braunschweig, Germany, 1999. Shaker-Verlag."},{"key":"15_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"154","DOI":"10.1007\/3-540-60275-5_63","volume-title":"TPHOL\u201995","author":"D. Eisenbiegler","year":"1995","unstructured":"D. Eisenbiegler, R. Kumar. An automata theory dedicated towards formal circuit synthesis.In TPHOL\u201995,number 971 in LNCS,pp. 154\u2013169, Aspen Grove, Utah, 1995. Springer."},{"key":"15_CR19","series-title":"Lect Notes Comput Sci","first-page":"154","volume-title":"TPHOLs\u201996","author":"D. Eisenbiegler","year":"1996","unstructured":"D. Eisenbiegler et al. Implementation issues about the embedding of existing high level synthesis algorithms in HOL. In TPHOLs\u201996, number 1125 in LNCS, pp. 154\u2013169, Turku, Finland, 1996. Springer."},{"key":"15_CR20","doi-asserted-by":"crossref","unstructured":"J. Gerlach, W. Rosenstiel. A Scalable Methodology for Cost Estimation in a Transformational High-Level Design Space Exploration Environment. In DATE\u201998, pp. 226\u2013231,Paris, France, 1998. IEEE Computer Society.","DOI":"10.1109\/DATE.1998.655861"},{"key":"15_CR21","unstructured":"http:\/\/goethe.ira.uka.de\/fsynth\/Charme\/<name>.c"},{"issue":"1","key":"15_CR22","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1109\/43.739056","volume":"18","author":"C. Blumenr\u00f6hr","year":"1999","unstructured":"C. Blumenr\u00f6hr et al. On the efficiency of formal synthesis \u2014experimental results. IEEE Transactions on CAD, 18(1):25\u201332, 1999.","journal-title":"IEEE Transactions on CAD"}],"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-48153-2_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,27]],"date-time":"2019-05-27T14:59:50Z","timestamp":1558969190000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48153-2_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540665595","9783540481539"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/3-540-48153-2_15","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[1999]]}}}