{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T16:20:30Z","timestamp":1743006030036,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540958901"},{"type":"electronic","value":"9783540958918"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-540-95891-8_46","type":"book-chapter","created":{"date-parts":[[2009,1,22]],"date-time":"2009-01-22T01:19:21Z","timestamp":1232587161000},"page":"509-520","source":"Crossref","is-referenced-by-count":4,"title":["Design Validation by Symbolic Simulation and Equivalence Checking: A Case Study in Memory Optimization for Image Manipulation"],"prefix":"10.1007","author":[{"given":"Kong Woei","family":"Susanto","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tim","family":"Todman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jose Gabriel","family":"Coutinho","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wayne","family":"Luk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"46_CR1","volume-title":"Computer-Aided Reasoning: ACL2 Case Studies","author":"D. Borrione","year":"2000","unstructured":"Borrione, D., Georgelin, P., Rodrigues, V.: Using Macros to Mimic VHDL. In: Computer-Aided Reasoning: ACL2 Case Studies. Kluwer Academic Publishers, Dordrecht (2000)"},{"key":"46_CR2","unstructured":"Canon, http:\/\/www.canon.co.uk"},{"key":"46_CR3","unstructured":"Cupak, M., Catthoor, F.: Verification of Loop Tranformations for Complex Data Dominated Applications. In: High Level Design Validation and Test, La Jolla, California, November 1998, pp. 72\u201379 (1998)"},{"key":"46_CR4","doi-asserted-by":"crossref","unstructured":"Dave, M.A.: Compiler verification: a bibliography. ACM SIGSOFT Software Engineering Notes\u00a028(6) (November 2003)","DOI":"10.1145\/966221.966235"},{"key":"46_CR5","unstructured":"Dutertre, B., Moura, L.: System Description: Yices 1.0, SRI International (2006)"},{"key":"46_CR6","unstructured":"hArtes, http:\/\/www.hartes.org"},{"issue":"8","key":"46_CR7","doi-asserted-by":"publisher","first-page":"701","DOI":"10.1007\/BF01191809","volume":"30","author":"C.A.R. Hoare","year":"1993","unstructured":"Hoare, C.A.R., He, J., Sampaio, A.: Normal form approach to compiler design. ACTA informatica\u00a030(8), 701\u2013739 (1993)","journal-title":"ACTA informatica"},{"issue":"4","key":"46_CR8","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1109\/54.936246","volume":"18","author":"N. Krishnamurthy","year":"2001","unstructured":"Krishnamurthy, N., Abadir, M.S., Martin, A.K., Abraham, J.A.: Design and Development Paradigm for Industrial Formal Verification CAD Tools. IEEE Design and Test of Computers\u00a018(4), 26\u201335 (2001)","journal-title":"IEEE Design and Test of Computers"},{"key":"46_CR9","doi-asserted-by":"crossref","unstructured":"Kurshan, R.P.: Formal Verification in a Commercial Setting. In: Proc. Design Automation Conference, Anaheim, pp. 258\u2013262 (1997)","DOI":"10.1109\/DAC.1997.597154"},{"key":"46_CR10","doi-asserted-by":"crossref","unstructured":"Lerner, S., Millstein, T., Chambers, C.: Automatically Proving the Correctness of Compiler Optimisations. In: Proc. Programming Language Design and Implementation, SanDiego, California (June 2003)","DOI":"10.1145\/781131.781156"},{"key":"46_CR11","doi-asserted-by":"crossref","unstructured":"Tristan, J.B., Leroy, X.: Formal verification of translation validators: A case study on instruction scheduling optimizations. In: Proc. 35th symposium Principles of Programming Languages, January 2008, pp. 17\u201327 (2008)","DOI":"10.1145\/1328438.1328444"},{"key":"46_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/3-540-49519-3_22","volume-title":"Formal Methods in Computer-Aided Design","author":"J.S. Moore","year":"1998","unstructured":"Moore, J.S.: Symbolic Simulation: An ACL2 Approach. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol.\u00a01522, pp. 334\u2013350. Springer, Heidelberg (1998)"},{"key":"46_CR13","doi-asserted-by":"crossref","unstructured":"Necula, G.C.: Translation Validation for an Optimizing Compiler. In: Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation, Vancouver, British Columbia (June 2000)","DOI":"10.1145\/349299.349314"},{"key":"46_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1007\/3-540-45937-5_16","volume-title":"Compiler Construction","author":"G.C. Necula","year":"2002","unstructured":"Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs. In: Horspool, R.N. (ed.) CC 2002. LNCS, vol.\u00a02304, p. 213. Springer, Heidelberg (2002)"},{"key":"46_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1007\/978-3-540-76650-6_17","volume-title":"Formal Methods and Software Engineering","author":"M. Oliveira","year":"2007","unstructured":"Oliveira, M., Woodcock, J.: Automatic generation of verified concurrent hardware. In: Butler, M., Hinchey, M.G., Larrondo-Petrie, M.M. (eds.) ICFEM 2007. LNCS, vol.\u00a04789, pp. 286\u2013306. Springer, Heidelberg (2007)"},{"key":"46_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"266","DOI":"10.1007\/978-3-540-76650-6_16","volume-title":"Formal Methods and Software Engineering","author":"J.I. Perna","year":"2007","unstructured":"Perna, J.I., Woodcock, J.: A Denotational Semantics for Handel-C Hardware Compilation. In: Butler, M., Hinchey, M.G., Larrondo-Petrie, M.M. (eds.) ICFEM 2007. LNCS, vol.\u00a04789, pp. 266\u2013285. Springer, Heidelberg (2007)"},{"key":"46_CR17","doi-asserted-by":"crossref","unstructured":"Saito, H., Ogawa, T., Sakunkonchack, T., Fujita, M., Nanya, T.: An Equivalence Checking Methodology for Hardware Oriented C-based Specifications. In: Proc. High-Level Design Validation and Test Workshop, October 2002, pp. 139\u2013144 (2002)","DOI":"10.1109\/HLDVT.2002.1224443"},{"key":"46_CR18","doi-asserted-by":"crossref","unstructured":"Singh, S., Lillieroth, C.J.: Formal Verification of Reconfigurable Cores. In: Proc. Field-Programmable Custom Computing Machines, Napa Valley, California, pp. 25\u201332 (1999)","DOI":"10.1109\/FPGA.1999.803664"},{"key":"46_CR19","doi-asserted-by":"crossref","unstructured":"Siegel, S.F., Mironova, A., Avrunin, G.S., Clarke, L.A.: Using Model Checking with Symbolic Execution to Verify Parallel Numerical Programs. In: Proc. International Symposium on Software Testing and Analysis, Portland (2006)","DOI":"10.1145\/1146238.1146256"},{"issue":"1","key":"46_CR20","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011132326153","volume":"19","author":"K.W. Susanto","year":"2001","unstructured":"Susanto, K.W., Melham, T.: Formally Analysed Dynamic Synthesis of Hardware. Journal of Supercomputing\u00a019(1), 7\u201322 (2001)","journal-title":"Journal of Supercomputing"},{"key":"46_CR21","unstructured":"Susanto, K.W., Luk, W., Coutinho, J.G., Todman, T.: Validating Design Optimisation. In: Proc. Tools and Techniques for Verification of System Infrastructure, London, March 2008, p. 36 (2008)"},{"key":"46_CR22","unstructured":"Stalmarck, G.: A System for Determining Propositional Logic Theorems by Applying Values and Rules to Triplets that are Generated from a Formula, Swedish Patent No. 467 076 (1992), U.S. Patent No 5 276 897 (1994), European Patent No 0403 454 (1995)"},{"key":"46_CR23","doi-asserted-by":"crossref","unstructured":"Todman, T., Coutinho, J.G., Luk, W.: Customisable Hardware Compilation. Journal of SuperComputing\u00a032 (2005)","DOI":"10.1007\/s11227-005-0288-x"},{"key":"46_CR24","unstructured":"Todman, T., Luk, W.: Memory Optimisations for High Resolution Imaging, in Proc. In: Proc. International Conference on Field-Programmable Technology, Brisbane, Australia (December 2004)"},{"key":"46_CR25","doi-asserted-by":"crossref","unstructured":"Zuck, L., Pnueli, A., Fang, Y., Goldberg, B., Hu, Y.: Translation and Run-Time Validation of Optimized Code. Electronic Notes in Theoretical Computer Science\u00a070(4) (2002)","DOI":"10.1016\/S1571-0661(04)80584-X"}],"container-title":["Lecture Notes in Computer Science","SOFSEM 2009: Theory and Practice of Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-95891-8_46","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,17]],"date-time":"2019-05-17T08:22:29Z","timestamp":1558081349000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-95891-8_46"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783540958901","9783540958918"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-95891-8_46","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}