{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T09:40:17Z","timestamp":1759138817479,"version":"3.44.0"},"reference-count":18,"publisher":"Elsevier BV","issue":"2","license":[{"start":{"date-parts":[[2002,5,1]],"date-time":"2002-05-01T00:00:00Z","timestamp":1020211200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2002,5,1]],"date-time":"2002-05-01T00:00:00Z","timestamp":1020211200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Integration"],"published-print":{"date-parts":[[2002,5]]},"DOI":"10.1016\/s0167-9260(02)00021-4","type":"journal-article","created":{"date-parts":[[2002,10,14]],"date-time":"2002-10-14T13:55:05Z","timestamp":1034603705000},"page":"101-131","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":0,"title":["A study about the efficiency of formal high-level synthesis applied to verification"],"prefix":"10.1016","volume":"31","author":[{"given":"Jos\u00e9 M.","family":"Mend\u0131\u0301as","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rom\u00e1n","family":"Hermida","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Olga","family":"Pe\u00f1alba","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"issue":"3","key":"10.1016\/S0167-9260(02)00021-4_BIB1","doi-asserted-by":"crossref","first-page":"239","DOI":"10.1023\/A:1008603713967","article-title":"The T-Ruby design system","volume":"11","author":"Sharp","year":"1997","journal-title":"Formal Methods Syst. Des."},{"key":"10.1016\/S0167-9260(02)00021-4_BIB2","series-title":"Formal Methods for VLSI Design","first-page":"13","article-title":"Circuit design in Ruby","author":"Jones","year":"1990"},{"key":"10.1016\/S0167-9260(02)00021-4_BIB3","doi-asserted-by":"crossref","unstructured":"L.C. Paulson, Isabelle: a Generic Theorem Prover, Lecture Notes in Computer Science, No. 828, Springer, Berlin, 1994.","DOI":"10.1007\/BFb0030541"},{"key":"10.1016\/S0167-9260(02)00021-4_BIB4","unstructured":"S.D. Johnson, B. Bose, DDD\u2014A system for mechanized digital design derivation, Proceeding of the International Workshop Formal Methods in VLSI Design 1991, Miami, FL, USA, January 1991."},{"key":"10.1016\/S0167-9260(02)00021-4_BIB5","doi-asserted-by":"crossref","unstructured":"J. Rees, W. Clinger, The revisited report on the algorithmic language Schema, ACM SIGPLAN Notices, No. 21\u201312, 1986, pp. 37\u201379.","DOI":"10.1145\/15042.15043"},{"issue":"1","key":"10.1016\/S0167-9260(02)00021-4_BIB6","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1109\/43.739056","article-title":"On the efficiency of formal synthesis\u2014experimental results","volume":"18","author":"Blumenr\u00f6hr","year":"1999","journal-title":"IEEE Trans. on Comput. -Aided Des. Integrated Circuits Sys."},{"key":"10.1016\/S0167-9260(02)00021-4_BIB7","unstructured":"M. Gordon, T. Melham, Introduction to HOL: a Theorem Proving Environment for Higher Order Logic, Cambridge University Press, Cambridge, July 1993."},{"issue":"1","key":"10.1016\/S0167-9260(02)00021-4_BIB8","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1023\/A:1008777509016","article-title":"Automated correctness condition generation for formal verification of synthesized RTL design","volume":"16","author":"Mansouri","year":"2000","journal-title":"Formal Methods Sys. Des."},{"key":"10.1016\/S0167-9260(02)00021-4_BIB9","doi-asserted-by":"crossref","unstructured":"H. Eveking, H. Hinrichsen, G. Ritter, Automatic verification of scheduling results in high-level synthesis, Proceedings of the Design Automation and Test in Europe Conference 1999, DATE\u201999, Munich, Germany, March 1999, pp. 59\u201364.","DOI":"10.1109\/DATE.1999.761097"},{"key":"10.1016\/S0167-9260(02)00021-4_BIB10","doi-asserted-by":"crossref","unstructured":"P. Ashar, et al., Verification of RTL generated from scheduled behavior in a high-level synthesis flow, Proceedings of the International Conference on Computer-Aided Design 1998, ICCAD\u201998, San Jose, CA, USA, November 1998, pp. 517\u2013524.","DOI":"10.1145\/288548.289080"},{"key":"10.1016\/S0167-9260(02)00021-4_BIB11","doi-asserted-by":"crossref","unstructured":"J.M. Mend\u0131\u0301as, R. Hermida, M. Fern\u00e1ndez, Correct high-level synthesis: a formal perspective, Proceedings of the Design Automation and Test in Europe Conference, DATE\u201998, Paris, France, 1998, pp. 977\u2013978.","DOI":"10.1109\/DATE.1998.655997"},{"key":"10.1016\/S0167-9260(02)00021-4_BIB12","unstructured":"C. Delgado, P.T. Breuer (Eds.), Formal Semantics for VHDL, Kluwer Academic Publishers, Dordrecht, 1995."},{"key":"10.1016\/S0167-9260(02)00021-4_BIB13","unstructured":"W.W. Wadge, E.A. Ashcroft, Lucid the Dataflow Programming Language, APIC Studies in data processing no 22, Academic Press, New York, 1985."},{"key":"10.1016\/S0167-9260(02)00021-4_BIB14","unstructured":"M. Wirsing, Algebraic specification: semantics, parameterization and refinement, in: Neuhold, E.J., Paul, M. (Eds.), Formal Description of Programming Concepts, IFIP State of the Art Reports, Springer, Berlin, 1991, pp. 259\u2013318."},{"key":"10.1016\/S0167-9260(02)00021-4_BIB15","doi-asserted-by":"crossref","unstructured":"J.V. Guttag, J.J. Horning (Ed.), Larch: Languages and Tools for Formal Specification, EATCS Monographs on Theoretical Computer Science, Springer, Berlin, 1993.","DOI":"10.1007\/978-1-4612-2704-5"},{"key":"10.1016\/S0167-9260(02)00021-4_BIB16","series-title":"Advanced Techniques for Embedded Systems Design and Test","first-page":"103","article-title":"Automatic formal derivation applied to high-level synthesis","author":"Mend\u0131\u0301as","year":"1998"},{"key":"10.1016\/S0167-9260(02)00021-4_BIB17","doi-asserted-by":"crossref","unstructured":"J.M. Mend\u0131\u0301as, R. Hermida, M. Fern\u00e1ndez, Formal techniques for hardware allocation, Proceedings of the Tenth International Conference on VLSI Design, VLSI\u201997, Hyderabad, India, January 1997, pp. 161\u2013165.","DOI":"10.1109\/ICVD.1997.568070"},{"key":"10.1016\/S0167-9260(02)00021-4_BIB18","doi-asserted-by":"crossref","unstructured":"O. Pe\u00f1alba, J.M. Mend\u0131\u0301as, M.C. Molina, Execution condition analysis in high level synthesis: a unified approach, Proceedings of the 13th International Symposium on System Synthesis, ISSS\u201900, Madrid, Spain, September 2000, pp. 73\u201378.","DOI":"10.1109\/ISSS.2000.874031"}],"container-title":["Integration"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167926002000214?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167926002000214?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T09:11:22Z","timestamp":1759137082000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0167926002000214"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,5]]},"references-count":18,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2002,5]]}},"alternative-id":["S0167926002000214"],"URL":"https:\/\/doi.org\/10.1016\/s0167-9260(02)00021-4","relation":{},"ISSN":["0167-9260"],"issn-type":[{"type":"print","value":"0167-9260"}],"subject":[],"published":{"date-parts":[[2002,5]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"A study about the efficiency of formal high-level synthesis applied to verification","name":"articletitle","label":"Article Title"},{"value":"Integration","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/S0167-9260(02)00021-4","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"converted-article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 2002 Elsevier Science B.V. All rights reserved.","name":"copyright","label":"Copyright"}]}}