{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,6]],"date-time":"2025-08-06T12:51:25Z","timestamp":1754484685631},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540569220"},{"type":"electronic","value":"9783540477877"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/3-540-56922-7_14","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T11:54:10Z","timestamp":1330257250000},"page":"166-179","source":"Crossref","is-referenced-by-count":32,"title":["Verification of a multiplier: 64 bits and beyond"],"prefix":"10.1007","author":[{"given":"R. P.","family":"Kurshan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Leslie","family":"Lamport","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,5,27]]},"reference":[{"key":"14_CR1","doi-asserted-by":"crossref","unstructured":"Martin Abadi and Leslie Lamport. Open systems. To appear in 1993 as a SRC Research Report.","DOI":"10.1145\/197917.197960"},{"issue":"8","key":"14_CR2","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"Randal E. E. Bryant","year":"1986","unstructured":"Randal E. Bryant. Graph-based algorithms for Boolean function manipulation. IEEE Transactions On Computers, C-35(8):677\u2013691, August 1986.","journal-title":"IEEE Transactions On Computers"},{"issue":"12","key":"14_CR3","doi-asserted-by":"crossref","first-page":"1529","DOI":"10.1109\/43.180266","volume":"11","author":"S. Chin","year":"1992","unstructured":"Shiu-Kai Chin. Verified functions for generating signed-binary arithmetic hardware. IEEE Transactions on Computer-Aided Design, 11(12):1529\u20131558, December 1992.","journal-title":"IEEE Transactions on Computer-Aided Design"},{"key":"14_CR4","series-title":"Lecture Notes in Computer Science","volume-title":"Computer-Aided Verification","author":"U. Engberg","year":"1992","unstructured":"Urban Engberg, Peter Gr\u00f8nning, and Leslie Lamport. Mechanical verification of concurrent systems with TLA. In Computer-Aided Verification, Lecture Notes in Computer Science, Berlin, Heidelberg, New York, June 1992. Springer-Verlag. Proceedings of the Fourth International Conference, CAV'92."},{"issue":"1","key":"14_CR5","doi-asserted-by":"crossref","first-page":"44","DOI":"10.1002\/j.1538-7305.1990.tb00102.x","volume":"69","author":"Z. Har'El","year":"1990","unstructured":"Z. Har'El and R. P. Kurshan. Software for analytical development of communication protocols. AT&T Technical Journal, 69(1):44\u201359, 1990.","journal-title":"AT&T Technical Journal"},{"key":"14_CR6","first-page":"286","volume-title":"S\/R: A language for specifying protocols and other coordinating processes","author":"J. Katzenelson","year":"1986","unstructured":"J. Katzenelson and R. P. Kurshan. S\/R: A language for specifying protocols and other coordinating processes. In Proceedings of the 5th Annual International Phoenix Conference on Computer Communications, pages 286\u2013292, Scottsdale, Arizona, 1986. IEEE Computer Society."},{"key":"14_CR7","volume-title":"Computer Arithmetic Algorithms","author":"I. Koren","year":"1993","unstructured":"Israel Koren. Computer Arithmetic Algorithms. Prentice Hall, Englewood Cliffs, New Jersey, 1993."},{"key":"14_CR8","first-page":"19","volume-title":"Discrete Event Systems: Models and Applications, volume 103 of Lecture Notes in Control and Information Sciences","author":"R. P. Kurshan","year":"1987","unstructured":"R. P. Kurshan. Reducibility in analysis of coordination. In P. Varaiya and A.B. Kurzhanski, editors, Discrete Event Systems: Models and Applications, volume 103 of Lecture Notes in Control and Information Sciences, pages 19\u201339, Berlin, 1987. Springer-Verlag."},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"R. P. Kurshan. Analysis of discrete event coordination. In J. W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Stepwise Refinement of Distributed Systems, volume 430 of Lecture Notes in Computer Science, pages 414\u2013453. Springer-Verlag, May\/June 1989.","DOI":"10.1007\/3-540-52559-9_74"},{"key":"14_CR10","doi-asserted-by":"crossref","unstructured":"R. P. Kurshan and K. McMillan. A structural induction theorem for processes. In Proceedings of the 8th annual ACM Symposium on Principles of Distributed Computing, pages 239\u2013247. ACM Press, 1989.","DOI":"10.1145\/72981.72998"},{"key":"14_CR11","first-page":"657","volume-title":"What good is temporal logic?","author":"L. Lamport","year":"1983","unstructured":"Leslie Lamport. What good is temporal logic? In R. E. A. Mason, editor, Information Processing 83: Proceedings of the IFIP 9th World Congress, pages 657\u2013668, Paris, September 1983. IFIP, North-Holland."},{"key":"14_CR12","unstructured":"Leslie Lamport. The temporal logic of actions. Research Report 79, Digital Equipment Corporation, Systems Research Center, December 1991."},{"key":"14_CR13","series-title":"Lecture Notes in Computer Science","volume-title":"Hybrid Systems","author":"L. Lamport","year":"1993","unstructured":"Leslie Lamport. Hybrid systems in TLA+. In Hans Rischel and Anders P. Ravn, editors, Hybrid Systems, Lecture Notes in Computer Science, Berlin, 1993. Springer-Verlag. Proceedings of a Workshop on Hybrid Systems, to appear."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-56922-7_14.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T00:57:32Z","timestamp":1619571452000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-56922-7_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540569220","9783540477877"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-56922-7_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1993]]}}}