{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,4]],"date-time":"2026-06-04T08:58:55Z","timestamp":1780563535599,"version":"3.54.1"},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540614630","type":"print"},{"value":"9783540685951","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/bfb0014319","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T09:04:25Z","timestamp":1132736665000},"page":"226-240","source":"Crossref","is-referenced-by-count":6,"title":["Using ghost variables to prove refinement"],"prefix":"10.1007","author":[{"given":"M.","family":"Marcus","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"A.","family":"Pnueli","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"issue":"2","key":"18_CR1","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1016\/0304-3975(91)90224-P","volume":"82","author":"M. Abadi","year":"1991","unstructured":"M. Abadi and L. Lamport. The existence of refinement mappings. Theoretical Computer Science, 82(2):253\u2013284, May 1991.","journal-title":"Theoretical Computer Science"},{"key":"18_CR2","doi-asserted-by":"crossref","unstructured":"J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors. Stepwise Refinement of Distributed Systems: Models, Formalism, Correctness. Lecture Notes in Computer Science 430. Springer-Verlag, 1990.","DOI":"10.1007\/3-540-52559-9"},{"key":"18_CR3","doi-asserted-by":"crossref","unstructured":"B. Jonsson. Modular verification of asynchronous networks. In Proc. 6th ACM Symp. Princ. of Dist. Comp., pages 152\u2013166, 1987.","DOI":"10.1145\/41840.41853"},{"key":"18_CR4","doi-asserted-by":"crossref","unstructured":"Y. Kesten, Z. Manna, and A. Pnueli. Temporal verification of simulation and refinement. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, A Decade of Concurrency, volume 803 of Lect. Notes in Comp. Sci., pages 273\u2013346. Springer-Verlag, 1994.","DOI":"10.1007\/3-540-58043-3_22"},{"key":"18_CR5","unstructured":"L. Lamport. The existence of refinement mapping. TLA Note 92-03-19, March 1992."},{"key":"18_CR6","unstructured":"P. Lucas. Two constructive realizations of the block concept and their equivalences. Technical Report Technical Report TR 25.085, IBM Laboratory Vienna, 1968."},{"issue":"1","key":"18_CR7","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1016\/0304-3975(91)90041-Y","volume":"83","author":"Z. Manna","year":"1991","unstructured":"Z. Manna and A. Pnueli. Completing the temporal picture. Theor. Comp. Sci., 83(1):97\u2013130, 1991.","journal-title":"Theor. Comp. Sci."},{"key":"18_CR8","volume-title":"The Temporal Logic of Reactive and Concurrent Systems: Specification","author":"Z. Manna","year":"1991","unstructured":"Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer-Verlag, New York, 1991."},{"key":"18_CR9","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-4222-2","volume-title":"Temporal Verification of Reactive Systems: Safety","author":"Z. Manna","year":"1995","unstructured":"Z. Manna and A. Pnueli. Temporal Verification of Reactive Systems: Safety. Springer-Verlag, New York, 1995."},{"key":"18_CR10","doi-asserted-by":"crossref","unstructured":"M. Marcus and A. Pnueli. Using ghost variables to prove refinement. Technical report, Weizmann Institute, 1996.","DOI":"10.1007\/BFb0014319"},{"key":"18_CR11","doi-asserted-by":"crossref","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"S. Owicki","year":"1976","unstructured":"S. Owicki and D. Gries. An axiomatic proof technique for parallel programs. Acta Informatica, 6:319\u2013340, 1976.","journal-title":"Acta Informatica"},{"key":"18_CR12","volume-title":"The Craft of Programming","author":"J.C. Reynolds","year":"1981","unstructured":"J.C. Reynolds. The Craft of Programming. Prentice-Hall, Engelwood Cliffs, NJ, 1981."}],"container-title":["Lecture Notes in Computer Science","Algebraic Methodology and Software Technology"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0014319","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T04:46:17Z","timestamp":1586580377000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0014319"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540614630","9783540685951"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/bfb0014319","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1996]]}}}