{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,12,30]],"date-time":"2024-12-30T05:40:30Z","timestamp":1735537230192,"version":"3.32.0"},"reference-count":33,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1993,6,1]],"date-time":"1993-06-01T00:00:00Z","timestamp":738892800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[1993,6]]},"DOI":"10.1007\/bf01384133","type":"journal-article","created":{"date-parts":[[2005,4,2]],"date-time":"2005-04-02T06:04:39Z","timestamp":1112421879000},"page":"231-257","source":"Crossref","is-referenced-by-count":12,"title":["Formal analysis of correctness of behavioral transformations"],"prefix":"10.1007","volume":"2","author":[{"given":"Michael C.","family":"McFarland","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"doi-asserted-by":"crossref","unstructured":"L. Nowak and P. Marwedel. Verification of hardware descriptions by retargetable code generation.Proceedings of the 26th Design Automation Conference, ACM\/IEEE, 1989, pp. 441?447.","key":"CR1","DOI":"10.1145\/74382.74456"},{"doi-asserted-by":"crossref","unstructured":"G.M. Brown and M.E. Leeser. From programs to transistors: Verifying hardware synthesis tools. pp. 129?151. InHardware Specification, Verification and Synthesis: Mathematical Aspects, Lecture Notes in Computer Science, 408: 129?151, 1989.","key":"CR2","DOI":"10.1007\/0-387-97226-9_27"},{"doi-asserted-by":"crossref","unstructured":"M. Genoe, L. Claesen, E. Verlind, F. Proesmans, and H. De Man. Illustration of the SFG-tracing multi-level behavioral verification methodology, by the correctness proof of a high to low level synthesis application in CATHEDRAL-II. InProceedings of the International Conference on Computer Design, IEEE, 1991, pp. 338?341.","key":"CR3","DOI":"10.1109\/ICCD.1991.139913"},{"doi-asserted-by":"crossref","unstructured":"G.J. Milne. The Correctness of a Simple Silicon Compiler. In6th IFIP International Symposium on Computer Hardware Description Languages and their Application 1983, pp. 1?12.","key":"CR4","DOI":"10.1016\/0167-7136(83)90174-9"},{"key":"CR5","volume-title":"Formal Aspects of VLSI Design","author":"P.A. Subrahmanyam","year":"1986","unstructured":"P.A. Subrahmanyam. The algebraic basis of an expert system for VLSI design. InFormal Aspects of VLSI Design, G. J. Milne and P.A. Subrahmanyam (eds.) North-Holland, New York, 1986."},{"key":"CR6","volume-title":"Synthesis of Digital Designs from Recursion Equations","author":"S.D. Johnson","year":"1984","unstructured":"S.D. Johnson.Synthesis of Digital Designs from Recursion Equations, Ph. D. thesis Indiana University, MIT Press, Cambridge, MA, 1984."},{"doi-asserted-by":"crossref","unstructured":"R. Milner.A calculus of communicating systems. Lecture Notes in Computer Science, 92, 1980.","key":"CR7","DOI":"10.1007\/3-540-10235-3"},{"issue":"7","key":"CR8","doi-asserted-by":"crossref","first-page":"621","DOI":"10.1109\/TC.1983.1676294","volume":"32","author":"M.C. McFarland","year":"1983","unstructured":"M.C. McFarland and A.C. Parker: An abstract model of behavior for hardware descriptions.IEEE Transactions on Computers C-32(7): 621?36, 1983.","journal-title":"IEEE Transactions on Computers C"},{"doi-asserted-by":"crossref","unstructured":"R. Vemuri. How to prove the completeness of a set of register level design transformations. InProceedings of the 27th Design Automation Conference, ACM\/IEEE, 1990, pp. 207?212.","key":"CR9","DOI":"10.1109\/DAC.1990.114855"},{"doi-asserted-by":"crossref","unstructured":"R. Camposano. Behavior-preserving transformations for high-level synthesis. InHardware Specification, Verification and Synthesis: Mathematical Aspects, Lecture Notes in Computer Science, 408: 1989.","key":"CR10","DOI":"10.1007\/0-387-97226-9_26"},{"unstructured":"D.W. Knapp and M. Winslett. A formalization of correctness for linked representations of datapath hardware. InProceedings of the 1989 IFIP WG 10.2\/WG 10.5 Conference on Applied Formal Methods for Correct VLSI Design, IFIP, 1989.","key":"CR11"},{"doi-asserted-by":"crossref","unstructured":"M.D. Aagaard and M.L. Leeser. A formally verified system for logic synthesis. InProceedings of the International Conference on Computer Design, IEEE, 1991.","key":"CR12","DOI":"10.1109\/ICCD.1991.139915"},{"key":"CR13","volume-title":"UT Year of Programming Institute on Concurrent Programming","author":"A.J. Martin","year":"1989","unstructured":"A.J. Martin. Programming in VLSI: From Communicating Processes to Delay-Insensitive Circuits. InUT Year of Programming Institute on Concurrent Programming, C.A.R. Hoare (ed.). Addision-Wesley, Reading, MA, 1989."},{"unstructured":"D.E. Thomas, E.M. Dirkes, R.A. Walker, J.V. Rajan, J.A. Nestor. and R.L. Blackburn. The system architect's workbench. InProceedings of the 25th Design Automation Conference, ACM\/IEEE, pp. 337?343. 1988.","key":"CR14"},{"doi-asserted-by":"crossref","unstructured":"E.D. Lagnese and D.E. Thomas. Architectural partitioning for system level design. InProceedings of the 26th Design Automation Conference, ACM\/IEEE, 1989, pp. 62?67.","key":"CR15","DOI":"10.1145\/74382.74394"},{"doi-asserted-by":"crossref","unstructured":"R.C. Sarma, M.D. Dooley, N.C. Newman, and G. Hetherington. High-level synthesis: Technology transfer to industry. InProceedings of the 27th Design Automation Conference ACM\/IEEE, 1990, pp. 549?554.","key":"CR16","DOI":"10.1145\/123186.123399"},{"doi-asserted-by":"crossref","unstructured":"T.E. Fuhrman. Industrial extensions to university high level synthesis tools: Making it work in the real world. InProceedings of the 28th Design Automation Conference ACM\/IEEE, 1991, pp. 520?525.","key":"CR17","DOI":"10.1145\/127601.127725"},{"issue":"1","key":"CR18","doi-asserted-by":"crossref","first-page":"24","DOI":"10.1109\/TC.1981.6312154","volume":"30","author":"M.R. Barbacci","year":"1981","unstructured":"M.R. Barbacci. Instruction set processor specifications (ISPS): The notation and its applications.IEEE Transactions on Computers, C-30(1):, 1981. 24?40.","journal-title":"IEEE Transactions on Computers, C"},{"unstructured":"M.C. McFarland.Mathematical Models for Verification in a Design Automation System. Ph. D. thesis, Carnegie-Mellon University, 1981.","key":"CR19"},{"doi-asserted-by":"crossref","unstructured":"R.W. Floyd. Assigning meaning to programs. InProceedings of the Symposium on Applied Mathematics 19, American Mathematical Society, 1967, pp. 19?32.","key":"CR20","DOI":"10.1090\/psapm\/019\/0235771"},{"unstructured":"M.C. McFarland. The VT: A database for Automated digital design. DRC-01-4-80, Design Research Centre, Carnegie-Mellon University, 1978.","key":"CR21"},{"unstructured":"M.R. Barbacci, G.E. Barnes, R.G. Cattell, and D.P. Siewiorek. The ISPS computer description language. Tech Report, Department of Computer Science, Carnegie-Mellon University, 1979.","key":"CR22"},{"unstructured":"M.C. McFarland. A Formal Definition of ISPS for Proving Properties of Hardware Descriptions, Department of Electrical Engineering, Carnegie-Mellon University, 1980.","key":"CR23"},{"key":"CR24","volume-title":"Hardware verification using high-order logic:From HDL Descriptions to Guaranteed Correct Circuit Designs","author":"A. Camilleri","year":"1987","unstructured":"A. Camilleri, M. Gordon, and T. Melham. Hardware verification using high-order logic:From HDL Descriptions to Guaranteed Correct Circuit Designs, D. Borrione, (ed.). North-Holland, New York, 1987."},{"doi-asserted-by":"crossref","unstructured":"D.J. Howe. Computational Metatheory in Nuprl. InProceedings of the 9th International Conference on Automated Deduction, Springer-Verlag, 1989, pp. 238?257.","key":"CR25","DOI":"10.1007\/BFb0012835"},{"unstructured":"E.A. Snow.Automation of Module Set Independent Register-Transfer Level Design. Ph.D. thesis, Carnegie-Mellon University, 1978.","key":"CR26"},{"doi-asserted-by":"crossref","unstructured":"E.A. Snow, D.P. Siewiorek, and D.E. Thomas. A technology-relative computer-aided design system: Abstract representations, transformations, and design tradeoffs. InProceedings of the 15th Design Automation Conference, ACM\/IEEE, 1978, pp. 220?226.","key":"CR27","DOI":"10.1109\/DAC.1978.1585173"},{"key":"CR28","volume-title":"The Irvine program transformation catalogue ? A stock of ideas for improving programs using source-to-source transformations","author":"T.A. Standish","year":"1976","unstructured":"T.A. Standish, D.C. Harriman, D.F. Kibler, and J.M. Neighbors. The Irvine program transformation catalogue ? A stock of ideas for improving programs using source-to-source transformations. Report No. 161, University of California, Irvine, 1976."},{"issue":"12","key":"CR29","doi-asserted-by":"crossref","first-page":"59","DOI":"10.1109\/MC.1983.1654268","volume":"16","author":"D.E. Thomas","year":"1983","unstructured":"D.E. Thomas, C.Y. III Hitchcock, T.J. Kowalski, J.V. Rajan, and R. Walker. Automatic data path synthesis.Computer 16(12): 59?70, 1983.","journal-title":"Computer"},{"issue":"10","key":"CR30","doi-asserted-by":"crossref","first-page":"1115","DOI":"10.1109\/43.39073","volume":"8","author":"R.A. Walker","year":"1989","unstructured":"R.A. Walker and D.E. Thomas. Behavioral transformations for algorithmic level IC design.IEEE Transactions on Computer-Aided Design, 8(10): 1115?1128, 1989.","journal-title":"IEEE Transactions on Computer-Aided Design"},{"unstructured":"J.D. Oakley.Symbolic Execution of Formal Machine Descriptions, Ph.D. thesis, Carnegie-Mellon University, 1979.","key":"CR31"},{"unstructured":"M.C. McFarland, and T.J. Kowalski. Assisting DAA: The use of global analysis in an expert system. InProceedings of the International Conference on Computer Design, IEEE 1986, pp. 482?485.","key":"CR32"},{"unstructured":"J.A. Nestor. Specification & synthesis of digital systems with interfaces. CMUCAD-87-10, Department of Electrical and Computer Engineering, Carnegie-Mellon University, 1987.","key":"CR33"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01384133.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01384133\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01384133","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,30]],"date-time":"2024-12-30T05:09:14Z","timestamp":1735535354000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01384133"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993,6]]},"references-count":33,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1993,6]]}},"alternative-id":["BF01384133"],"URL":"https:\/\/doi.org\/10.1007\/bf01384133","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[1993,6]]}}}