{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,3]],"date-time":"2026-10-03T20:20:34Z","timestamp":1791058834004,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540614746","type":"print"},{"value":"9783540685999","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/3-540-61474-5_78","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T21:41:11Z","timestamp":1330292471000},"page":"300-310","source":"Crossref","is-referenced-by-count":16,"title":["Protocol verification by aggregation of distributed transactions"],"prefix":"10.1007","author":[{"given":"Seungjoon","family":"Park","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David L.","family":"Dill","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2005,6,3]]},"reference":[{"key":"26_CR1","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"82","author":"M. Abadi","year":"1991","unstructured":"Mart\u00edn Abadi and Leslie Lamport. The existence of refinement mappings. Theoretical Computer Science, 82:253\u2013284, 1991.","journal-title":"Theoretical Computer Science"},{"key":"26_CR2","doi-asserted-by":"crossref","unstructured":"Jerry Burch and David Dill Automatic verification of pipelined microprocessor control. In Computer Aided Verification, 6th International Conference, CAV'94, pages 68\u201380, June 1994.","DOI":"10.1007\/3-540-58179-0_44"},{"key":"26_CR3","volume-title":"PhD thesis","author":"E. Cohen","year":"1993","unstructured":"Ernest Cohen. Modular progress proofs of asynchronous programs. PhD thesis, University of Texas at Austin, 1993."},{"key":"26_CR4","doi-asserted-by":"crossref","unstructured":"J. de Bakker, W. de Roever, and G. Rozenberg, editors. Stepwise Refinement of Distributed Systems. Models, Formalisms, Correctness.: LNCS 430. Springer-Verlag, 1990.","DOI":"10.1007\/3-540-52559-9"},{"key":"26_CR5","doi-asserted-by":"crossref","unstructured":"D. Dill, A. Drexler, A. Hu, and C. Yang. Protocol verification as a hardware design aid. In International Conference on Computer Design: VLSI in Computers. IEEE Computer Society, 1992.","DOI":"10.1109\/ICCD.1992.276232"},{"key":"26_CR6","doi-asserted-by":"crossref","unstructured":"D. Dill, A. Hu, and H. Wong-Toi. Checking for language inclusion using simulation relation. In Computer Aided Verification, 3rd International Workshop, pages 255\u2013265, July 1991.","DOI":"10.1007\/3-540-55179-4_25"},{"key":"26_CR7","unstructured":"Mark Heinrich. The FLASH Protocol. Internal document, Stanford University FLASH Group, 1993."},{"key":"26_CR8","unstructured":"C. Norris Ip and David Dill. State reduction using reversible rules. In Proceedings of 33rd Design Automation Conference, June 1996."},{"key":"26_CR9","doi-asserted-by":"crossref","unstructured":"J. Kuskin, D. Ofelt, M. Heinrich, J. Heinlein, R. Simoni, K. Gharachorloo, J. Chapin, D. Nakahira, J. Baxter, M. Horowitz, A. Gupta, M. Rosenblum, and J. Hennessy. The Stanford FLASH multiprocessor. In Proc. 21st International Symposium on Computer Architecture, pages 302\u2013313, April 1994.","DOI":"10.1109\/ISCA.1994.288140"},{"key":"26_CR10","doi-asserted-by":"crossref","unstructured":"Robert Kurshan. Computer-Aided Verification of Coordinating Processes: The Automata-Theoretic Approach. Princeton, 1994.","DOI":"10.1515\/9781400864041"},{"key":"26_CR11","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1016\/0167-6423(83)90014-X","volume":"2","author":"L. Lamport","year":"1982","unstructured":"Leslie Lamport. An assertional correctness proof of a distributed algorithm. Science of Computer Programming, 2:175\u2013206, 1982.","journal-title":"Science of Computer Programming"},{"issue":"2","key":"26_CR12","doi-asserted-by":"publisher","first-page":"190","DOI":"10.1145\/69624.357207","volume":"5","author":"L. Lamport","year":"1983","unstructured":"Leslie Lamport. Specifying concurrent program modules. ACM Transactions on Programming Language and Systems, 5(2): 190\u2013222, April 1983.","journal-title":"ACM Transactions on Programming Language and Systems"},{"key":"26_CR13","unstructured":"P. Ladkin, L. Lamport, B. Olivier, and D. Roegel. Lazy caching: An assertional view. Distributed Computing, 1996. To appear."},{"issue":"4","key":"26_CR14","doi-asserted-by":"crossref","first-page":"325","DOI":"10.1109\/TSE.1984.5010246","volume":"10","author":"S. Lam","year":"1984","unstructured":"S. Lam and A. Shankar. Protocol verification via projection. IEEE Transactions on Software Engineering, 10(4):325\u2013342, July 1984.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"26_CR15","doi-asserted-by":"crossref","unstructured":"N. Lynch. I\/O automata: A model for discrete event systems. In 22nd Annual Conference on Information Science and Systems, March 1988. Princeton University.","DOI":"10.21236\/ADA196047"},{"key":"26_CR16","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K. McMillan","year":"1993","unstructured":"Ken McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993. Boston."},{"issue":"2","key":"26_CR17","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1109\/32.345827","volume":"21","author":"S. Owre","year":"1995","unstructured":"S. Owre, J. Rushby, N. Shankar, and F. von Henke. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21(2):107\u2013125, February 1995.","journal-title":"IEEE Transactions on Software Engineering"},{"key":"26_CR18","unstructured":"Seungjoon Park and David Dill. Verification of FLASH cache coherence protocol by aggregation of distributed transactions. In Proc. 8th ACM Symposium on Parallel Algorithms and Architectures, June. 1996."},{"key":"26_CR19","doi-asserted-by":"crossref","unstructured":"D. Peled, S. Katz, and A. Pnueli. Specifying and proving serializability in temporal logic. In Proc. 6th Annual IEEE Symposium on Logic in Computer Science, pages 232\u2013244, July 1991.","DOI":"10.1109\/LICS.1991.151648"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-61474-5_78.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:06:41Z","timestamp":1605647201000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-61474-5_78"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540614746","9783540685999"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/3-540-61474-5_78","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996]]}}}