{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T13:11:49Z","timestamp":1754485909238},"publisher-location":"Berlin, Heidelberg","reference-count":17,"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_51","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:01:20Z","timestamp":1330275680000},"page":"223-238","source":"Crossref","is-referenced-by-count":3,"title":["A formal framework for high level synthesis"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Kropf","sequence":"first","affiliation":[]},{"given":"Klaus","family":"Schneider","sequence":"additional","affiliation":[]},{"given":"Ramayya","family":"Kumar","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"key":"13_CR1","unstructured":"M.C. McFarland, A.C. Parker, and R. Camposano. Tutorial on high-level synthesis. In 25th Design Automation Conference, pages 330\u2013336, 1988."},{"key":"13_CR2","doi-asserted-by":"crossref","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, and D.L. Dill. Sequential circuit verification using symbolic model checking. 27rd ACM\/IEEE Design Automation Conference. IEEE, 1990, pages 46\u201351.","DOI":"10.1145\/123186.123223"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"A. Gupta. Formal hardware verification methods: A survey. Journal of Formal Methods in System Design, pages 151\u2013238, 1992.","DOI":"10.1007\/BF00121125"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"K. Schneider, R. Kumar, and T. Kropf. Automating verification by functional abstraction at the system level. In T. Melham and J. Camilleri, editors, International Workshop on Higher Order Logic Theorem Proving and its Applications, pages 391\u2013406, Malta, September 1994. Lecture Notes on Computer Science No. 859, Springer.","DOI":"10.1007\/3-540-58450-1_56"},{"key":"13_CR5","series-title":"IFIP TC10\/WG10.2","first-page":"419","volume-title":"Modelling generic hardware structures by abstract datatypes","author":"K. Schneider","year":"1992","unstructured":"K. Schneider, R. Kumar, and T. Kropf. Modelling generic hardware structures by abstract datatypes. In L. Claesen and M. Gordon, editors, International Workshop on Higher Order Logic Theorem Proving and its Applications, pages 419\u2013429, Leuven, Belgium, September 1992. IFIP TC10\/WG10.2, Elsevier Science Publishers."},{"key":"13_CR6","first-page":"355","volume-title":"volume 575 of Lecture Notes in Computer Science","author":"M. Mutz","year":"1991","unstructured":"M. Mutz. Using the HOL theorem proving environment for proving the correctness of term rewriting rules reducing terms of sequential behavior. In K.G. Larsen and A. Skou. International Workshop on Computer Aided Verification, volume 575 of Lecture Notes in Computer Science. Springer, Aalborg, July 1991, pages 355\u2013366."},{"key":"13_CR7","first-page":"59","volume-title":"Integration of formal methods with system design","author":"E. Mayger","year":"1991","unstructured":"E. Mayger and M. P. Fourman. Integration of formal methods with system design. In A. Halaas and P.B. Denyer. International Conference on Very Large Scale Integration, pages 59\u201370, 1991. Edinburgh, North-Holland."},{"key":"13_CR8","series-title":"IFIP WG 10.2","first-page":"265","volume-title":"Computer Hardware Description Languages and their Applications","author":"M. Fujita","year":"1989","unstructured":"M. Fujita and H. Fujisawa. Specification, verification and synthesis of control circuits with propositional temporal logic. J.A. Darringer and F.J. Rammig, editors. Computer Hardware Description Languages and their Applications, Washington, June 1989. IFIP WG 10.2, North-Holland, pages 265\u2013279."},{"key":"13_CR9","series-title":"IFIP WG 10.2","first-page":"99","volume-title":"The Fusion of Hardware Design and Verification","author":"S.M. Burns","year":"1988","unstructured":"S.M. Burns and A.J. Martin. Synthesis of self-timed circuits by program transformation. In G. Milne, editor, The Fusion of Hardware Design and Verification, pages 99\u2013116, Glasgow, Scotland, July 1988. IFIP WG 10.2, North-Holland."},{"key":"13_CR10","unstructured":"M.J.C. Gordon and T. Melham. Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, 1993."},{"key":"13_CR11","unstructured":"F.K. Hanna and N. Daeche. Specification and verification using high-order logic. In C.J. Koomen and T. Moto-oka, editors, Computer Hardware Description Languages, pages 418\u2013433. Elsevier Science Publishers, North-Holland, 1985."},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"E. A. Emerson. Temporal and Modal Logics, chapter 16, pages 996\u20131072. Elsevier Science Publishers, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"F. Kr\u00f6ger. Temporal Logic of Programs, volume 8 of EATCS Monographs on Theoretical Computer Science. Springer Verlag, 1987.","DOI":"10.1007\/978-3-642-71549-5_5"},{"key":"13_CR14","first-page":"648","volume-title":"Control-path oriented verification of sequential generic circuits with control and data path","author":"K. Schneider","year":"1994","unstructured":"K. Schneider, T. Kropf, and R. Kumar. Control-path oriented verification of sequential generic circuits with control and data path. In 4th European Design Automation Conference, pages 648\u2013652, Paris, France, March 1994. IEEE Computer Society Press."},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"T. Melham. Abstraction mechanisms for hardware verification. In G. Birtwistle and P.A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis, pages 267\u2013291. Kluwer Academic Press, 1988.","DOI":"10.1007\/978-1-4613-2007-4_9"},{"key":"13_CR16","unstructured":"K. Schneider, T. Kropf, and R. Kumar. Why hardware verification needs more than model checking. In International Workshop on Higher Order Logic Theorem Proving and its Applications, Malta, 1994, Short Paper."},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"R. Kumar, K. Schneider, and T. Kropf. Structuring and automating hardware proofs in a higher-order theorem-proving environment. International Journal of Formal System Design, pages 165\u2013230, 1993.","DOI":"10.1007\/BF01383880"}],"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_51.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:25:24Z","timestamp":1605648324000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-59047-1_51"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540590477","9783540491774"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-59047-1_51","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}