{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,24]],"date-time":"2026-03-24T06:00:55Z","timestamp":1774332055139,"version":"3.50.1"},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2001,5,1]],"date-time":"2001-05-01T00:00:00Z","timestamp":988675200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2001,5,1]],"date-time":"2001-05-01T00:00:00Z","timestamp":988675200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["The Journal of Supercomputing"],"published-print":{"date-parts":[[2001,5]]},"DOI":"10.1023\/a:1011184310224","type":"journal-article","created":{"date-parts":[[2002,12,23]],"date-time":"2002-12-23T03:43:03Z","timestamp":1040614983000},"page":"23-39","source":"Crossref","is-referenced-by-count":11,"title":["An Approach to the Specification and Verification of a Hardware Compilation Scheme"],"prefix":"10.1007","volume":"19","author":[{"given":"Jonathan P.","family":"Bowen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"He","family":"Jifeng","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"333396_CR1","doi-asserted-by":"crossref","unstructured":"F. Balarin, M. Chiodo, P. Giusto, H. Hsieh, A. Jurecska, L. Lavagno, C. Passerone, A. Sangiovanni-Vincentelli, E. Sentovich, K. Suzuki, and B. Tabbara. Hardware-software Co-design of Embedded Systems: The Polis approach, Kluwer International Series in Engineering and Computer Science, 1997.","DOI":"10.1007\/978-1-4615-6127-9"},{"key":"333396_CR2","doi-asserted-by":"crossref","unstructured":"G. Berry. The foundations of Esterel. In G. Plotkin, C. Stirling, and M. Tofte, eds., Proof, language and interaction: Essays in honour of Robin Milner, MIT Press, 425-454, 2000.","DOI":"10.7551\/mitpress\/5641.003.0021"},{"key":"333396_CR3","unstructured":"J. P. Bowen, ed. Towards Verified Systems, Real-Time Safety Critical Systems series, Vol. 2, Elsevier Science, 1994."},{"issue":"4","key":"333396_CR4","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1145\/332051.332078","volume":"43","author":"J. P. Bowen","year":"2000","unstructured":"J. P. Bowen. The ethics of safety-critical systems. Communcations of the ACM, 43(4):91-97, April 2000.","journal-title":"Communcations of the ACM"},{"key":"333396_CR5","series-title":"Technical Report","volume-title":"Hardware compilation: Verification and rapid-prototyping","author":"J. P. Bowen","year":"1999","unstructured":"J. P. Bowen and H. Jifeng. Hardware compilation: Verification and rapid-prototyping. Technical Report RUCS\/1999\/TR\/012\/A, Department of Computer Science, The University of Reading, UK, October 1999."},{"key":"333396_CR6","doi-asserted-by":"crossref","unstructured":"J. P. Bowen, H. Jifeng, and I. Page. Hardware compilation. In [3], Chapter 10, pp. 193-207, 1994.","DOI":"10.1016\/B978-0-444-89901-9.50019-7"},{"key":"333396_CR7","doi-asserted-by":"crossref","unstructured":"J. P. Bowen, H. Jifeng, and X. Qiwen. An animatable operational semantics of the Verilog Hardware Description Language. In Shaoying Liu, J. A. McDermid and M. G. Hinchey, eds., Proc. ICFEM2000: 3rd IEEE International Conference on Formal Engineering Methods, York, UK, 4\u20136 September 2000, pp. 199-207. IEEE Computer Society Press, 2000.","DOI":"10.1109\/ICFEM.2000.873820"},{"key":"333396_CR8","doi-asserted-by":"crossref","unstructured":"J. P. Bowen and M. G. Hinchey. High-Integrity System Specification and Design, Formal Approaches to Computing and Information Technology (FACIT) series, Springer-Verlag, 1999.","DOI":"10.1007\/978-1-4471-3431-2"},{"key":"333396_CR9","doi-asserted-by":"crossref","unstructured":"P. T. Breuer, N. Martinez Madrid, J. P. Bowen, R. France, M. Larrondo Petrie, and C. Delgado Kloos, Reasoning about VHDL and VHDL-AMS using denotational semantics. In D. Borrione, ed., DATE'99: Design, Automation & Test in Europe, Munich, Germany, 9\u201312 March 1999, pages 346-352, ACM, 1999.","DOI":"10.1109\/DATE.1999.761144"},{"key":"333396_CR10","unstructured":"Celoxica. Handel-C: Product Information Sheet, Milton Park, Abingdon, Oxfordshire, UK, 2001. URL: http:\/\/www.celoxica.com"},{"key":"333396_CR11","first-page":"563","volume":"1349","author":"A. Cerone","year":"1997","unstructured":"A. Cerone, A. J. Cowie, and G. J. Milne. The Circal system. In Proc. 6th International Conference on Algebraic Methodologies and Software Technology (AMAST'97), Sydney, Australia, 13\u201317 December 1997. Lecture Notes in Computer Science, Vol. 1349, pp. 563-564. Springer-Verlag, 1997.","journal-title":"Proc. 6th International Conference on Algebraic Methodologies and Software Technology (AMAST'97)"},{"issue":"6","key":"333396_CR12","doi-asserted-by":"crossref","first-page":"12","DOI":"10.1109\/MC.2014.157","volume":"31","author":"L. Garber","year":"1998","unstructured":"L. Garber and D. Sims. In pursuit of hardware-software codesign. IEEE Computer, 31(6):12-14, June 1998.","journal-title":"IEEE Computer"},{"key":"333396_CR13","unstructured":"H. Jifeng. Provably Correct Systems: Modelling of Communication Languages and Design of Optimized Compilers, McGraw-Hill International Series in Software Engineering, 1995."},{"key":"333396_CR14","unstructured":"H. Jifeng. A common framework for mixed hardware\/software systems. In K. Araki, A. Galloway and K. Taguchi, eds., IFM 99: Proceedings of the 1st International Conference on Integrated Formal Methods, York, 28\u201329 June 1999, pp. 1-15. Springer-Verlag, 1999."},{"key":"333396_CR15","doi-asserted-by":"crossref","unstructured":"H. Jifeng. A behavioral model for co-design. In J. M. Wing, J. Woodcock and J. Davis, eds., FM'99-Formal Methods, Lecture Notes in Computer Science, Vol. 1709, pp. 1420-1438. Springer-Verlag, 1999.","DOI":"10.1007\/3-540-48118-4_25"},{"issue":"6","key":"333396_CR16","doi-asserted-by":"crossref","first-page":"643","DOI":"10.1007\/BF03259390","volume":"6","author":"H. Jifeng","year":"1994","unstructured":"H. Jifeng and J. P. Bowen. Specification, verification and prototyping of an optimized compiler. Formal Aspects of Computing, 6(6):643-658, 1994.","journal-title":"Formal Aspects of Computing"},{"key":"333396_CR17","doi-asserted-by":"crossref","unstructured":"H. Jifeng, I. Page, and J. P. Bowen. Towards a provably correct hardware implementation of Occam. In G. J. Milne and L. Pierre, eds., Correct Hardware Design and Verification Methods, Lecture Notes in Computer Science, Vol. 683, pp. 214-226. Springer-Verlag, 1993.","DOI":"10.1007\/BFb0021726"},{"key":"333396_CR18","doi-asserted-by":"crossref","unstructured":"M. G. Hinchey and J. P. Bowen, eds. Industrial-Strength Formal Methods in Practice, Formal Approaches to Computing and Information Technology (FACIT) series, Springer-Verlag, 1999.","DOI":"10.1007\/978-1-4471-0523-7"},{"issue":"8\u20139","key":"333396_CR19","doi-asserted-by":"crossref","first-page":"525","DOI":"10.1016\/0165-6074(96)00009-9","volume":"41","author":"C. A. R. Hoare","year":"1996","unstructured":"C. A. R. Hoare. The logic of engineering design. Microprocessing and Microprogramming, 41(8\u20139): 525-539, 1996.","journal-title":"Microprocessing and Microprogramming"},{"key":"333396_CR20","unstructured":"C. A. R. Hoare and H. Jifeng. Unifying Theories of Programming, Prentice Hall Series in Computer Science, 1998."},{"key":"333396_CR21","doi-asserted-by":"crossref","unstructured":"C. A. R. Hoare and I. Page. Hardware and software: Closing the gap. Transputer Communications, 69-90, June 1994.","DOI":"10.1007\/3-540-57840-4_24"},{"key":"333396_CR22","doi-asserted-by":"crossref","unstructured":"J. Iyoda, A. Sampaio, and L. Silva. ParTS: A partitioning transformation system. In J. M. Wing, J. Woodcock and J. Davis, eds., FM'99-Formal Methods, Lecture Notes in Computer Science, Vol. 1709 pp. 1400-1419. Springer-Verlag, 1999.","DOI":"10.1007\/3-540-48118-4_24"},{"issue":"2","key":"333396_CR23","doi-asserted-by":"crossref","first-page":"270","DOI":"10.1145\/3318.3322","volume":"7","author":"G. Milne","year":"1985","unstructured":"G. Milne. CIRCAL and the representation of communication, concurrency and time. ACM Transactions on Programming Languages and Systems, 7(2):270-298, 1985.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"1","key":"333396_CR24","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1007\/BF00936948","volume":"12","author":"I. Page","year":"1996","unstructured":"I. Page. Constructing hardware-software systems from a single description. Journal of VLSI Signal Processing, 12(1):87-107, 1996.","journal-title":"Journal of VLSI Signal Processing"},{"key":"333396_CR25","first-page":"271","volume-title":"FPGAs","author":"I. Page","year":"1991","unstructured":"I. Page and W. Luk. Compiling Occam into Field-Programmable Gate Arrays. In W. Moore and W. Luk, eds., FPGAs, pp. 271-284. Abingdon EE&CS Books, Abingdon, UK, 1991."},{"key":"333396_CR26","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1016\/0304-3975(88)90049-7","volume":"60","author":"A. W. Roscoe","year":"1988","unstructured":"A. W. Roscoe and C. A. R. Hoare. Laws of Occam programming. Theoretical Computer Science, 60: 177-229, 1988.","journal-title":"Theoretical Computer Science"},{"key":"333396_CR27","volume-title":"A Generic Approach to Compiling Occam into Circuits","author":"P. Shaw","year":"1994","unstructured":"P. Shaw. A Generic Approach to Compiling Occam into Circuits. PhD thesis, Department of Computer Science, University of Strathclyde, UK, December 1994."},{"key":"333396_CR28","doi-asserted-by":"crossref","unstructured":"P. Shaw and G. Milne. A highly parallel FPGA-based machine and its formal verification. In Proc. FPL92, pp. 162-173, 1992.","DOI":"10.1007\/3-540-57091-8_41"},{"key":"333396_CR29","doi-asserted-by":"crossref","unstructured":"J. Staunstrup and W. Wolf, eds. Hardware\/Software Co-design: Principles and practice, Kluwer Academic Publishers, 1997.","DOI":"10.1007\/978-1-4757-2649-7"},{"issue":"6","key":"333396_CR30","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1109\/2.683004","volume":"31","author":"N. Wirth","year":"1998","unstructured":"N. Wirth. Hardware compilation: Translating programs into circuits. IEEE Computer, 31(6):25-31, June 1998.","journal-title":"IEEE Computer"},{"key":"333396_CR31","unstructured":"Xilinx, Inc. Spartan Series FPGAs, San Jose, California, USA, 1999. URL: http:\/\/www.xilinx.com\/ products\/spartan.htm"}],"container-title":["The Journal of Supercomputing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1011184310224.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1011184310224\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1011184310224.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,8]],"date-time":"2025-08-08T05:16:50Z","timestamp":1754630210000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1011184310224"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,5]]},"references-count":31,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2001,5]]}},"alternative-id":["333396"],"URL":"https:\/\/doi.org\/10.1023\/a:1011184310224","relation":{},"ISSN":["0920-8542","1573-0484"],"issn-type":[{"value":"0920-8542","type":"print"},{"value":"1573-0484","type":"electronic"}],"subject":[],"published":{"date-parts":[[2001,5]]}}}