{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:10:28Z","timestamp":1725664228661},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540590477"},{"type":"electronic","value":"9783540491774"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/3-540-59047-1_52","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T17:00:50Z","timestamp":1330275650000},"page":"239-257","source":"Crossref","is-referenced-by-count":1,"title":["Tutorial on design verification with synchronized transitions"],"prefix":"10.1007","author":[{"given":"Niels","family":"Mellergaard","sequence":"first","affiliation":[]},{"given":"J\u00f8rgen","family":"Staunstrup","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,6,1]]},"reference":[{"key":"14_CR1","unstructured":"Robert S. Boyer and J. Strother Moore. A Computational Logic. Academic Press, 1979."},{"key":"14_CR2","unstructured":"Robert S. Boyer and J. Strother Moore. A Computational Logic Handbook. Academic Press, 1988."},{"key":"14_CR3","unstructured":"Randal E. Bryant. Can a simulator verify a circuit? In Formal Aspects of VLSI Design, pages 125\u2013136. North-Holland, 1985."},{"key":"14_CR4","doi-asserted-by":"crossref","unstructured":"K. Mani Chandy and Jajadev Misra. Parallel Program Design: A Foundation. Addison-Wesley, 1988.","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"14_CR5","doi-asserted-by":"crossref","unstructured":"R.W. Floyd. Assigning meanings to programs. In J.T. Schwartz, editor, Proceedings of the Symposium in Applied Mathematics, volume 19, pages 19\u201332. American Mathematical Society, 1967.","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"14_CR6","unstructured":"Michael P. Fourman and Robert L. Harris. Lambda \u2014 logic and mathematics behind design automation. In Proceedings of the 26th ACM\/IEEE design Automation Conference. ACM, 1989."},{"key":"14_CR7","doi-asserted-by":"crossref","unstructured":"Stephen J. Garland and John V. Guttag. An overview of LP: the Larch Prover. In Proceedings of the Third International Conference on Rewriting Techniques and Applications. Springer-Verlag, 1989.","DOI":"10.1007\/3-540-51081-8_105"},{"key":"14_CR8","unstructured":"Mike Gordon. Why higher-order logic is a good formalism for specifying and verifying hardware. In Formal Aspects of VLSI Design, pages 153\u2013177. North-Holland, 1985."},{"issue":"2\/3","key":"14_CR9","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1007\/BF00121125","volume":"1","author":"A. Gupta","year":"1992","unstructured":"Aarti Gupta. Formal hardware verification methods: A survey. Formal Methods in Systems Design, 1(2\/3):151\u2013238, October 1992.","journal-title":"Formal Methods in Systems Design"},{"key":"14_CR10","unstructured":"John V. Guttag, James J. Horning with S.J. Garland, K.D. Jones, A. Modet, and J.M. Wing. Larch: Languages and Tools for Formal Specification. Springer-Verlag Texts and Monographs in Computer Science, 1993. ISBN 0-387-94006-5, ISBN 3-540-94006-5."},{"key":"14_CR11","unstructured":"Warren A. Hunt. FM8501: A verified microprocessor. In From HDL Descriptions to Guaranteed Correct Circuit Designs, pages 85\u2013114. North-Holland, 1986."},{"key":"14_CR12","unstructured":"Niels Maretti. Mechanized verification of refinement. In Proceedings from TPCD '94, 1994. To appear."},{"key":"14_CR13","unstructured":"Niels Mellergaard. Mechanized Design Verification. PhD thesis, Department of Computer Science, Technical University of Denmark, 1994."},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"J\u00f8rgen Staunstrup. A Formal Approach to Hardware Design. Kluwer Academic Publishers, 1994.","DOI":"10.1007\/978-1-4615-2764-0"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"J\u00f8rgen Staunstrup, Stephen J. Garland, and John V. Guttag. Localized verification of circuit descriptions. In Proceedings of the Workshop on Automatic Verification Methods for Finite State Systems, LNCS 407. Springer Verlag, 1989.","DOI":"10.1007\/3-540-52148-8_29"},{"key":"14_CR16","unstructured":"J\u00f8rgen Staunstrup, Stephen J. Garland, and John V. Guttag. Mechanized verification of circuit descriptions using the Larch Prover. In V. Stavridou and T. Melham, editors, Proceedings of the IFIP WG 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, pages 277\u2013300. Elsevier, 1992."},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"J\u00f8rgen Staunstrup and Niels Mellergaard. Localized verification of modular designs. Formal Methods in System Design, 1994. accepted for publication.","DOI":"10.1007\/BF01384501"}],"container-title":["Lecture Notes in Computer Science","Theorem Provers in Circuit Design"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-59047-1_52.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:25:25Z","timestamp":1605648325000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-59047-1_52"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540590477","9783540491774"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/3-540-59047-1_52","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1995]]}}}