{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:03:17Z","timestamp":1754481797318,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540649878"},{"type":"electronic","value":"9783540498018"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1998]]},"DOI":"10.1007\/bfb0055147","type":"book-chapter","created":{"date-parts":[[2006,7,27]],"date-time":"2006-07-27T09:09:13Z","timestamp":1153991353000},"page":"367-386","source":"Crossref","is-referenced-by-count":6,"title":["On the effectiveness of theorem proving guided discovery of formal assertions for a register allocator in a high-level synthesis system"],"prefix":"10.1007","author":[{"given":"Naren","family":"Narasimhan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ranga","family":"Vemuri","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,5,27]]},"reference":[{"key":"22_CR1","unstructured":"C.-J Tseng and D. P. Siewiorek. Automated Synthesis of Data Paths in Digital Systems. In IEEE Transactions on CAD, July 1986."},{"key":"22_CR2","doi-asserted-by":"crossref","unstructured":"D. Eisenbiegler, C. Blumenrohr, and R. Kumar. Implementation Issues about the Embedding of Existing High Level Synthesis Algorithms in HOL. In TPHOL. Springer, 1996.","DOI":"10.1007\/BFb0105403"},{"key":"22_CR3","doi-asserted-by":"crossref","unstructured":"D. Gries. The Science of Programming. Springer-Verlag, 1981.","DOI":"10.1007\/978-1-4612-5983-1"},{"key":"22_CR4","doi-asserted-by":"crossref","unstructured":"D. D. Gajski, N. D. Dutt, A. C. Wu and S. Y. Lin. High-level Synthesis, Introduction to Chip and System Design. Kluwer Academic Publishers, 1992.","DOI":"10.1007\/978-1-4615-3636-9_1"},{"key":"22_CR5","doi-asserted-by":"crossref","unstructured":"D. L. Springer and D. E. Thomas. Exploiting the Special Structure of Conflict and Compatibility Graphs in High-Level Synthesis. In Proceedings of ICCAD, pages 254\u2013157, 1990.","DOI":"10.1109\/ICCAD.1990.129895"},{"key":"22_CR6","unstructured":"E. M. Mayger and M. P. Fourman. Integration of Formal Methods with System Design. In A. Halaax and P. B. Denyer, editor, International Conference on VLSI, pages 59\u201370. IFIP Transactions, August 1991."},{"key":"22_CR7","doi-asserted-by":"crossref","unstructured":"D. E. Thomas et al. Algorithmic and Register Transfer Level Synthesis: The System Architect's Workbench. Kluwer Academic Publishers, 1990.","DOI":"10.1007\/978-1-4613-1519-3_8"},{"key":"22_CR8","unstructured":"F. K. Hanna, M. Longley and N. Daeche. Formal Synthesis of Digital Systems. In Workshop on Applied Formal Methods for Correct VLSI Design, pages 532\u2013548. IMEC-IFIP, Elsevier Science Publishers B.V., 1989."},{"key":"22_CR9","doi-asserted-by":"crossref","unstructured":"M. C. Golumbic. Algorithmic Graph Theory and Perfect Graphs. Academic Press, 1980.","DOI":"10.1016\/B978-0-12-289260-8.50010-8"},{"key":"22_CR10","doi-asserted-by":"crossref","unstructured":"J. Roy, N. Kumar, R. Dutta and R. Vemuri. DSS: A Distributed High-Level Synthesis System. In IEEE Design and Test of Computers, June 1992.","DOI":"10.1109\/54.143143"},{"volume-title":"Introduction to HOL","year":"1993","key":"22_CR11","unstructured":"M. Gordon and T. Melham, editor. Introduction to HOL. Cambridge Univ. Press, Cambridge, England, 1993."},{"key":"22_CR12","doi-asserted-by":"crossref","unstructured":"M. Larsson. An Engineering Approach to Formal System Design. In Thomas F. Melham and Juanito Camilleri, editor, Higher Order Logic Theorem Proving and its Applications, pages 300\u2013315. Springer, September 1994.","DOI":"10.1007\/3-540-58450-1_50"},{"key":"22_CR13","volume-title":"Computers and Intractability","author":"M. R. Garey","year":"1979","unstructured":"M. R. Garey and D. S. Johnson. Computers and Intractability. W. H. Freeman and Company, New York, 1979."},{"key":"22_CR14","doi-asserted-by":"crossref","unstructured":"N. Narasimhan and R. Vemuri. Synchronous Controller Models for Synthesis from Communicating VHDL Processes. In Ninth International Conference on VLSI Design, pages 198\u2013204, Bangalore, India, January 1996.","DOI":"10.1109\/ICVD.1996.489484"},{"key":"22_CR15","unstructured":"N. Narasimhan, R. Kalyanaraman, and R. Vemuri. Validation of Synthesized Register-Transfer Level Designs Using Simulation and Formal Verification. In High Level Design Validation and Test Workshop, November 1996."},{"key":"22_CR16","doi-asserted-by":"crossref","unstructured":"R. Camposano and W. Wolf. High-Level VLSI Synthesis. Kluwer Academic Publishers, 1991.","DOI":"10.1007\/978-1-4615-3966-7"},{"key":"22_CR17","doi-asserted-by":"crossref","unstructured":"R. Vemuri et al. Experiences in Functional Validation of a High Level Synthesis System. In 30th ACM\/IEEE Design Automation Conference, pages 194\u2013201, 1993.","DOI":"10.1145\/157485.164667"},{"key":"22_CR18","doi-asserted-by":"crossref","unstructured":"S. Owre, J. M. Rushby, and N. Shankar. PVS: A Prototype Verification System. In Deepak Kapur, editor, 11th International Conference on Automated Deduction (CADE), volume 607, pages 748\u2013752. Springer-Verlag, June 1992.","DOI":"10.1007\/3-540-55602-8_217"},{"key":"22_CR19","unstructured":"S. D. Johnson. Synthesis of Digital Designs from Recursion Equations. MIT, 1984."},{"key":"22_CR20","unstructured":"S. D. Johnson, R. M. Wehrmeister and Bhaskar Bose. On the Interplay of Synthesis and Verification. In Workshop on Applied Formal Methods for Correct VLSI Design, pages 385\u2013404. IMEC-IFIP, Elsevier Science Publishers B.V., 1989."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0055147","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T03:14:14Z","timestamp":1736478854000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0055147"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1998]]},"ISBN":["9783540649878","9783540498018"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/bfb0055147","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1998]]}}}