{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T21:04:22Z","timestamp":1776373462708,"version":"3.51.2"},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2006,7,14]],"date-time":"2006-07-14T00:00:00Z","timestamp":1152835200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2007,2,7]]},"DOI":"10.1007\/s10009-006-0005-y","type":"journal-article","created":{"date-parts":[[2006,7,13]],"date-time":"2006-07-13T15:33:07Z","timestamp":1152804787000},"page":"37-51","source":"Crossref","is-referenced-by-count":16,"title":["Compositional software verification based on game semantics and process algebra"],"prefix":"10.1007","volume":"9","author":[{"given":"Aleksandar","family":"Dimovski","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ranko","family":"Lazi\u0107","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2006,7,14]]},"reference":[{"key":"5_CR1","volume-title":"Semantics and Logics of Computation","author":"S. Abramsky","year":"1997","unstructured":"Abramsky S.(1997). Semantics of interaction. In: Dybjer P., Pitts A. (eds) Semantics and Logics of Computation. University Press, Cambridge"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"Abramsky, S., McCusker, G.: Linearity, sharing and state: a fully abstract game semantics for Idealized Algol with active expressions. In: O\u2019Hearn, P.W., Tennent, R.D. (eds.) Algol-like languages. Birkh\u00e4user (1997)","DOI":"10.1007\/978-1-4757-3851-3_10"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Abramsky, S.: Algorithmic game semantics: a tutorial introduction. Lecture notes, Marktoberdorf International Summer School (2001)","DOI":"10.1007\/978-94-010-0413-8_2"},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"Abramsky, S., Ghica, D., Murawski, A., Ong, C.-H.L.: Applying game semantics to compositional software modeling and verifications. In: Proceedings of TACAS, LNCS vol. 2988, pp. 421\u2013435 (2004)","DOI":"10.1007\/978-3-540-24730-2_32"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Appel, A.W., Palsberg, J.: Modern Compiler Implementation in Java, 2nd edn. Cambridge University Press (2002)","DOI":"10.1017\/CBO9780511811432"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"Ball, T., Rajamani, S.K.: The SLAM project debugging system software via static analysis. In: Proceedings of POPL, ACM SIGPLAN Notices, vol. 37(1), pp.~1\u20133 (2002)","DOI":"10.1145\/565816.503274"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Proceedings of Logic of Programs Workshop, LNCS vol.131, pp.~52\u201371 (1981)","DOI":"10.1007\/BFb0025774"},{"key":"5_CR8","volume-title":"Model Checking","author":"E.M. Clarke","year":"2000","unstructured":"Clarke E.M., Grumberg O., Peled D.(2000): Model Checking. MIT Press, Cambridge"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"Dimovski, A., Ghica, D., Lazi\u0107, R.: Data-abstraction refinement: a game semantic approach. In: Proceedings of SAS, LNCS vol.~3672, pp.~102\u2013117 (2005)","DOI":"10.1007\/11547662_9"},{"key":"5_CR10","unstructured":"Formal Systems (Europe) Ltd, Failures-Divergence Refinement: FDR2 Manual (2000)"},{"issue":"1\u20133","key":"5_CR11","doi-asserted-by":"crossref","first-page":"469","DOI":"10.1016\/S0304-3975(03)00315-3","volume":"309","author":"D. Ghica","year":"2003","unstructured":"Ghica D., McCusker G. (2003): The regular-language semantics of second-order idealized Algol. Theor. Comput. Sci. 309(1\u20133): 469\u2013502","journal-title":"Theor. Comput. Sci."},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"Ghica, D., Murawski, A., Ong, C.-H.L.: Syntactic Control of Concurrency. In: Proceedings of ICALP, LNCS vol. 3142, pp.~683\u2013694 (2004)","DOI":"10.1007\/978-3-540-27836-8_58"},{"key":"5_CR13","volume-title":"Communicating Sequential Processes","author":"C.A.R. Hoare","year":"1985","unstructured":"Hoare C.A.R.(1985): Communicating Sequential Processes. Prentice Hall, Englewood Cliffs"},{"key":"5_CR14","doi-asserted-by":"crossref","first-page":"285","DOI":"10.1006\/inco.2000.2917","volume":"163","author":"J.M.E. Hyland","year":"2000","unstructured":"Hyland J.M.E., Ong C.-H.L.(2000): On full abstraction for PCF: I, II and III. Inform. Comput. 163: 285\u2013400","journal-title":"Inform. Comput."},{"key":"5_CR15","unstructured":"Laird, J.: A Semantic Analysis of Control. PhD thesis, University of Edinburgh (1998)"},{"key":"5_CR16","unstructured":"Lazi\u0107, R.: A Semantic Study of Data Independence with Applications to Model Checking. DPhil thesis, Computing Laboratory, Oxford University (1999)"},{"key":"5_CR17","unstructured":"Murawski, A., Walukiewicz, I.: Third-order Idealized Algol with iteration is decidable. In: Proceedings of FoSSaCS, LNCS vol. 3411, 202\u2013218 (2004)"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"Quielle, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Proceedings of the 5th International Symposium on Programming, pp.~337\u2013351 (1982)","DOI":"10.1007\/3-540-11494-7_22"},{"key":"5_CR19","unstructured":"Reynolds, J.C.: The essence of Algol. In: Proceedings of ISAL, 345\u2013372 (1981)"},{"key":"5_CR20","doi-asserted-by":"crossref","unstructured":"Roscoe, A.W., Gardiner, P.H.B., Goldsmith, M.H., Hulance, J.R., Jackson, D.M., Scattergood, J.B.: Hierarchical compression for model-checking CSP or how to check 1020 dining philosophers for deadlock. In: Proceedings of TACAS, LNCS vol. 1019, 133\u2013152 (1995)","DOI":"10.1007\/3-540-60630-0_7"},{"key":"5_CR21","volume-title":"The Theory and Practice of Concurrency","author":"A.W. Roscoe","year":"1998","unstructured":"Roscoe A.W.(1998): The Theory and Practice of Concurrency. Prentice Hall, Englewood Cliffs"},{"key":"5_CR22","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proceedings of 1st LICS, 332\u2013344 (1986)"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-006-0005-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-006-0005-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-006-0005-y","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,16]],"date-time":"2020-04-16T17:50:28Z","timestamp":1587059428000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-006-0005-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,7,14]]},"references-count":22,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2007,2,7]]}},"alternative-id":["5"],"URL":"https:\/\/doi.org\/10.1007\/s10009-006-0005-y","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006,7,14]]}}}