{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,12,31]],"date-time":"2022-12-31T09:17:50Z","timestamp":1672478270763},"reference-count":14,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[1993,12,1]],"date-time":"1993-12-01T00:00:00Z","timestamp":754704000000},"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,12]]},"DOI":"10.1007\/bf01384073","type":"journal-article","created":{"date-parts":[[2005,4,2]],"date-time":"2005-04-02T04:20:31Z","timestamp":1112415631000},"page":"181-209","source":"Crossref","is-referenced-by-count":10,"title":["Using transformations and verification in circuit design"],"prefix":"10.1007","volume":"3","author":[{"given":"James B.","family":"Saxe","sequence":"first","affiliation":[]},{"given":"James J.","family":"Horning","sequence":"additional","affiliation":[]},{"given":"John V.","family":"Guttag","sequence":"additional","affiliation":[]},{"given":"Stephen J.","family":"Garland","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"9","key":"CR1","doi-asserted-by":"crossref","first-page":"1044","DOI":"10.1109\/32.58789","volume":"16","author":"Stephen J. Garland","year":"1990","unstructured":"Stephen J. Garland, John V. Guttag, and James J. Horning. Debugging Larch Shared Language specifications.IEEE Transactions on Software Engineering, 16(9):1044?1057, september 1990.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"CR2","first-page":"329","volume-title":"Proceedings of the IFIP WG 10.2 Conference on the Fusion of Hardware Design and Verification","author":"Stephen J. Garland","year":"1988","unstructured":"Stephen J. Garland, John V. Guttag, and J\u00f8rgen Staunstrup. Verification of VLSI circuits using LP.Proceedings of the IFIP WG 10.2 Conference on the Fusion of Hardware Design and Verification. Amsterdam, North Holland, 1988, pp. 329?345."},{"key":"CR3","unstructured":"John Rushby and Friedrich von Henke. Formal verification of the interactive convergence clock synchronization algorithm usingehdm. SRI International report SRI-CSL-89-3, February, 1989."},{"key":"CR4","unstructured":"Stephen J. garland and John V. Guttag. A guide to LP, the Larch Prover. Digital Equipment Corp. Systems Research Center, SRC Report 82, December 1991."},{"key":"CR5","volume-title":"A Computational Logic Handbook","author":"Robert S. Boyer","year":"1988","unstructured":"Robert S. Boyer and J. Strother Moore.A Computational Logic Handbook. Academic Press, New York, 1988."},{"key":"CR6","volume-title":"VLSI Specification, Verification and Synthesis","author":"M.J.C. Gordon. HOL","year":"1988","unstructured":"M.J.C. Gordon. HOL: A proof generating system for higher-order logic. InVLSI Specification, Verification and Synthesis, G. Birtwistle and P.A. Subrahmanyam, (eds.). Kluwer, Boston, 1988."},{"issue":"1","key":"CR7","first-page":"41","volume":"1","author":"Charles E. Leiserson","year":"1983","unstructured":"Charles E. Leiserson and James B. Saxe. Optimizing synchronous systems.Journal of VLSI and Computer Systems, 1(1):41?67, Spring 1983","journal-title":"Journal of VLSI and Computer Systems"},{"issue":"1","key":"CR8","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1007\/BF01759032","volume":"6","author":"Charles E. Leiserson","year":"1991","unstructured":"Charles E. Leiserson and James B. Saxe. Retiming synchronous circuity.Algorithmica, 6(1):5?35, 1991.","journal-title":"Algorithmica"},{"key":"CR9","doi-asserted-by":"crossref","unstructured":"David Detlefs and Randy Forgaard. A Procedure for automatically proving the termination of a set of rewrite rules.Proceedings of the first International Conference on Rewriting Techniques and Applications, Dijon, France.Lecture Notes in Computer Science, 202:255?270, May 1985.","DOI":"10.1007\/3-540-15976-2_12"},{"key":"CR10","doi-asserted-by":"crossref","unstructured":"Avra Cohn. The notion of proof in hardware verfication.Journal of Automated Reasoning, 5(2): 127?139.","DOI":"10.1007\/BF00243000"},{"key":"CR11","first-page":"71","volume-title":"Formal Methods for VLSI Design","author":"J\u00f8rgen Staunstrup","year":"1990","unstructured":"J\u00f8rgen Staunstrup and Mark Greenstreet. Synchronized Transitions. InFormal Methods for VLSI Design, J\u00f8rgen Staunstrup, (ed.), Amsterdam, North-Holland\/Elservier, 1990, pp. 71?129."},{"issue":"4","key":"CR12","first-page":"429","volume":"5","author":"Warren A. Hunt Jr.","year":"1980","unstructured":"Warren A. Hunt, Jr. Microprocessor design verification.Journal of Automated Reasoning, 5(4): 429?460, December 1980.","journal-title":"Journal of Automated Reasoning"},{"issue":"3","key":"CR13","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1016\/0167-9260(89)90004-7","volume":"7","author":"Jeffrey J. Joyce","year":"1989","unstructured":"Jeffrey J. Joyce. Formal specification and verification of microprocessor systems.Integration, the VLSI Journal, 7(3):247?266, September 1989.","journal-title":"Integration, the VLSI Journal"},{"key":"CR14","first-page":"289","volume-title":"The Fusion of Hardware Design and Verification","author":"Mary Sheeran","year":"1988","unstructured":"Mary Sheeran. Retiming and slowdown in Ruby. InThe Fusion of Hardware Design and Verification, George J. Milne, (ed.) Amsterdam, North-Holland, 1988, pp. 289?308."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01384073.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/BF01384073\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BF01384073","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,6]],"date-time":"2020-04-06T16:26:57Z","timestamp":1586190417000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BF01384073"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993,12]]},"references-count":14,"journal-issue":{"issue":"3","published-print":{"date-parts":[[1993,12]]}},"alternative-id":["BF01384073"],"URL":"https:\/\/doi.org\/10.1007\/bf01384073","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993,12]]}}}