{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,14]],"date-time":"2025-05-14T18:43:36Z","timestamp":1747248216039,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":42,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540212997"},{"type":"electronic","value":"9783540247302"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2004]]},"DOI":"10.1007\/978-3-540-24730-2_32","type":"book-chapter","created":{"date-parts":[[2010,8,2]],"date-time":"2010-08-02T15:00:15Z","timestamp":1280761215000},"page":"421-435","source":"Crossref","is-referenced-by-count":37,"title":["Applying Game Semantics to Compositional Software Modeling and Verification"],"prefix":"10.1007","author":[{"given":"Samson","family":"Abramsky","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dan R.","family":"Ghica","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrzej S.","family":"Murawski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"C. -H. Luke","family":"Ong","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"32_CR1","doi-asserted-by":"crossref","unstructured":"Abramsky, S., Jagadeesan, R., Malacaria, P.: Full abstraction for PCF. Information and Computation\u00a0163 (2000)","DOI":"10.1006\/inco.2000.2930"},{"key":"32_CR2","doi-asserted-by":"crossref","unstructured":"Hyland, J.M.E., Ong, C.H.L.: On full abstraction for PCF: I, II and III. Information and Computation\u00a0163 (2000)","DOI":"10.1006\/inco.2000.2917"},{"key":"32_CR3","series-title":"ENTCS","volume-title":"Proc. of 1996 Workshop on Linear Logic","author":"S. Abramsky","year":"1996","unstructured":"Abramsky, S., McCusker, G.: Linearity, sharing and state: a fully abstract game semantics for Idealized Algol with active expressions. In: Proc. of 1996 Workshop on Linear Logic. ENTCS, vol.\u00a03, Elsevier, Amsterdam (1996); Also [22, Chap. 20]"},{"key":"32_CR4","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0304-3975(99)00047-X","volume":"227","author":"S. Abramsky","year":"1999","unstructured":"Abramsky, S., McCusker, G.: Full abstraction for Idealized Algol with passive expressions. Theoretical Computer Science\u00a0227, 3\u201342 (1999)","journal-title":"Theoretical Computer Science"},{"key":"32_CR5","doi-asserted-by":"crossref","unstructured":"Abramsky, S., Honda, K., McCusker, G.: A fully abstract game semantics for general references. In: Proc. of LICS 1998 (1998)","DOI":"10.1109\/LICS.1998.705669"},{"key":"32_CR6","doi-asserted-by":"crossref","unstructured":"Laird, J.: Full abstraction for functional languages with control. In: Proc. of LICS 1997, pp. 58\u201367 (1997)","DOI":"10.1109\/LICS.1997.614931"},{"key":"32_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/BFb0055067","volume-title":"Automata, Languages and Programming","author":"C. Hankin","year":"1998","unstructured":"Hankin, C., Malacaria, P.: Generalised flowcharts and games. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol.\u00a01443, p. 363. Springer, Heidelberg (1998)"},{"key":"32_CR8","doi-asserted-by":"crossref","unstructured":"Hankin, C., Malacaria, P.: Non-deterministic games and program analysis: an application to security. In: Proc. of LICS 1999, pp. 443\u2013452 (1999)","DOI":"10.1109\/LICS.1999.782639"},{"key":"32_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/3-540-45022-X_10","volume-title":"Automata, Languages and Programming","author":"D.R. Ghica","year":"2000","unstructured":"Ghica, D.R., McCusker, G.: Reasoning about Idealized algol using regular languages. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol.\u00a01853, p. 103. Springer, Heidelberg (2000)"},{"key":"32_CR10","series-title":"ENTCS","first-page":"85","volume-title":"17th MFPS","author":"D.R. Ghica","year":"2001","unstructured":"Ghica, D.R.: Regular language semantics for a call-by-value programming language. In: 17th MFPS, Aarhus, Denmark. ENTCS, vol.\u00a045, pp. 85\u201398. Elsevier, Amsterdam (2001)"},{"key":"32_CR11","unstructured":"Ghica, D.R.: A regular-language model for Hoare-style correctness statements. In: Proc. of the Verification and Computational Logic 2001, Florence, Italy (2001)"},{"key":"32_CR12","unstructured":"Ghica, D.R.: A Games-based Foundation for Compositional Software Model Checking. PhD thesis, Queen\u2019s University School of Computing, Kingston, Ontario, Canada (2002)"},{"key":"32_CR13","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (1999)"},{"key":"32_CR14","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1145\/251595.251617","volume":"32","author":"D.A. Schmidt","year":"1997","unstructured":"Schmidt, D.A.: On the need for a popular formal semantics. ACM SIGPLAN Notices\u00a032, 115\u2013116 (1997)","journal-title":"ACM SIGPLAN Notices"},{"key":"32_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"390","DOI":"10.1007\/3-540-61474-5_86","volume-title":"Computer Aided Verification","author":"D.L. Dill","year":"1996","unstructured":"Dill, D.L.: The Mur\u03c6 verfication system. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 390\u2013393. Springer, Heidelberg (1996)"},{"key":"32_CR16","series-title":"Lecture Notes in Computer Science","first-page":"385","volume-title":"Computer Aided Verification","author":"G.J. Holzmann","year":"1996","unstructured":"Holzmann, G.J., Peled, D.A.: The state of SPIN. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 385\u2013389. Springer, Heidelberg (1996)"},{"key":"32_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"521","DOI":"10.1007\/BFb0028774","volume-title":"Computer Aided Verification","author":"R. Alur","year":"1998","unstructured":"Alur, R., Henzinger, T.A., Mang, F.Y.C., Qadeer, S.: MOCHA: Modularity in model checking. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 521\u2013525. Springer, Heidelberg (1998)"},{"key":"32_CR18","first-page":"58","volume-title":"Proc. of 29th POPL","author":"T.A. Henzinger","year":"2002","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Lazy abstraction. In: Proc. of 29th POPL, pp. 58\u201370. ACM Press, New York (2002)"},{"key":"32_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/3-540-44585-4_25","volume-title":"Computer Aided Verification","author":"T. Ball","year":"2001","unstructured":"Ball, T., Rajamani, S.K.: The SLAM toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 260\u2013275. Springer, Heidelberg (2001)"},{"key":"32_CR20","doi-asserted-by":"crossref","first-page":"439","DOI":"10.1145\/337180.337234","volume-title":"Proc. of the 22nd International Conference on Software Engineering","author":"J.C. Corbett","year":"2000","unstructured":"Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., P\u0103s\u0103reanu, C.S., Zheng, H.: Bandera. In: Proc. of the 22nd International Conference on Software Engineering, pp. 439\u2013448. ACM Press, New York (2000)"},{"key":"32_CR21","first-page":"345","volume-title":"Algorithmic Languages, Proc. of the International Symposium on Algorithmic Languages","author":"J.C. Reynolds","year":"1981","unstructured":"Reynolds, J.C.: The essence of Algol. In: de Bakker, J.W., van Vliet, J.C. (eds.) Algorithmic Languages, Proc. of the International Symposium on Algorithmic Languages, pp. 345\u2013372. North-Holland, Amsterdam (1981)"},{"volume-title":"Algol-like Languages. Progress in Theoretical Computer Science, Two volumes","year":"1997","key":"32_CR22","unstructured":"O\u2019Hearn, P.W., Tennent, R.D. (eds.): Algol-like Languages. Progress in Theoretical Computer Science, Two volumes. Birkh\u00e4user, Boston (1997)"},{"key":"32_CR23","unstructured":"Abramsky, S.: Algorithmic game semantics: A tutorial introduction. Lecture notes, Marktoberdorf International Summer School 2001 (2001)"},{"key":"32_CR24","volume-title":"Introduction to Automata Theory, Languages, and Computation","author":"J.E. Hopcroft","year":"1979","unstructured":"Hopcroft, J.E., Ullman, J.D.: Introduction to Automata Theory, Languages, and Computation. Addison-Wesley, Reading (1979)"},{"key":"32_CR25","doi-asserted-by":"crossref","unstructured":"Reape, M., Thompson, H.S.: Parallel intersection and serial composition of finite state transducers. In: COLING 1988, pp. 535\u2013539 (1988)","DOI":"10.3115\/991719.991749"},{"key":"32_CR26","doi-asserted-by":"crossref","unstructured":"Ong, C.H.L.: Observational equivalence of third-order Idealized Algol is decidable. In: Proc. of LICS 2002, pp. 245\u2013256 (2002)","DOI":"10.1109\/LICS.2002.1029833"},{"key":"32_CR27","unstructured":"Ghica, D.R., McCukser, G.: The regular-language semantics of first-order Idealized algol. Theoretical Computer Science (to appear)"},{"key":"32_CR28","unstructured":"Murawski, A.S.: Variable scope and call-by-value program equivalence (2003) (in preparation)"},{"key":"32_CR29","doi-asserted-by":"crossref","unstructured":"Senizergues: L(A) = L(B)? decidability results from complete formal systems. TCS: Theoretical Computer Science 251 (2001)","DOI":"10.1016\/S0304-3975(00)00285-1"},{"key":"32_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"821","DOI":"10.1007\/3-540-45465-9_70","volume-title":"Automata, Languages and Programming","author":"C. Stirling","year":"2002","unstructured":"Stirling, C.: Deciding DPDA equivalence is primitive recursive. In: Widmayer, P., Triguero, F., Morales, R., Hennessy, M., Eidenbenz, S., Conejo, R. (eds.) ICALP 2002. LNCS, vol.\u00a02380, pp. 821\u2013865. Springer, Heidelberg (2002)"},{"key":"32_CR31","volume-title":"Proc. of LICS 2003","author":"A.S. Murawski","year":"2003","unstructured":"Murawski, A.S.: On program equivalence in languages with ground-type references. In: Proc. of LICS 2003, IEEE Computer Society Press, Los Alamitos (2003)"},{"key":"32_CR32","unstructured":"Murawski, A.S.: Complexity of first-order call-by-name program equivalence (2003) (submitted for publication)"},{"key":"32_CR33","unstructured":"AT&T FSM Library tm \u2013 general-purpose finite-state machine software tools, http:\/\/www.research.att.com\/sw\/tools\/fsm\/"},{"key":"32_CR34","unstructured":"Ghica, D.R.: Game-based software model checking: Case studies and methodological considerations. Technical Report PRG-RR-03-11, Oxford University Computing Laboratory (2003)"},{"key":"32_CR35","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1023\/A:1026599015809","volume":"13","author":"J. Hatcliff","year":"2000","unstructured":"Hatcliff, J., Dwyer, M.B., Zheng, H.: Slicing software for model construction. Higher-Order and Symbolic Computation\u00a013, 315\u2013353 (2000)","journal-title":"Higher-Order and Symbolic Computation"},{"key":"32_CR36","doi-asserted-by":"publisher","first-page":"377","DOI":"10.1145\/93385.93442","volume-title":"Proc. of the 9th Annual ACM Symposium on Principles of Distributed Computing","author":"Z. Manna","year":"1990","unstructured":"Manna, Z., Pnueli, A.: A hierarchy of temporal properties. In: Dwork, C. (ed.) Proc. of the 9th Annual ACM Symposium on Principles of Distributed Computing, Qu\u00e9bec City, Qu\u00e9bec, Canada, pp. 377\u2013408. ACM Press, New York (1990)"},{"key":"32_CR37","doi-asserted-by":"crossref","unstructured":"Colby, C., Godefroid, P., Jagadeesan, L.: Automatically closing open reactive programs. In: Proc. of PLDI 1998, Montreal, Canada, pp. 345\u2013357 (1998)","DOI":"10.1145\/277650.277754"},{"key":"32_CR38","series-title":"Software Engineering Notes","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1145\/503209.503226","volume-title":"Proc. of the 9th ESEC\/FSE 2001","author":"L. Alfaro de","year":"2001","unstructured":"de Alfaro, L., Henzinger, T.A.: Interface automata. In: Gruhn, V. (ed.) Proc. of the 9th ESEC\/FSE 2001. Software Engineering Notes, vol.\u00a026(5), pp. 109\u2013120. ACM Press, New York (2001)"},{"key":"32_CR39","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1145\/585265.585270","volume":"49","author":"R. Alur","year":"2002","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. of the ACM\u00a049, 672\u2013713 (2002)","journal-title":"J. of the ACM"},{"key":"32_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"211","DOI":"10.1007\/978-3-540-24727-2_16","volume-title":"Foundations of Software Science and Computation Structures","author":"D.R. Ghica","year":"2004","unstructured":"Ghica, D.R., Murawski, A.S.: Angelic semantics of fine-grained concurrency. In: Walukiewicz, I. (ed.) FOSSACS 2004. LNCS, vol.\u00a02987, pp. 211\u2013225. Springer, Heidelberg (2004) (to appear)"},{"key":"32_CR41","unstructured":"Lazic, R.S.: A Semantic Study of Data Independence with Applications to Model Checking. PhD thesis, University of Oxford (1999)"},{"key":"32_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"581","DOI":"10.1007\/3-540-44618-4_41","volume-title":"CONCUR 2000 - Concurrency Theory","author":"R. Lazic","year":"2000","unstructured":"Lazic, R., Nowak, D.: A unifying approach to data-independence. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol.\u00a01877, p. 581. Springer, Heidelberg (2000)"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-24730-2_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,23]],"date-time":"2025-02-23T18:00:15Z","timestamp":1740333615000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-24730-2_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004]]},"ISBN":["9783540212997","9783540247302"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-24730-2_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2004]]}}}