{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,12]],"date-time":"2025-01-12T00:40:15Z","timestamp":1736642415222,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":22,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540474609"},{"type":"electronic","value":"9783540474623"}],"license":[{"start":{"date-parts":[[2006,1,1]],"date-time":"2006-01-01T00:00:00Z","timestamp":1136073600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11901433_29","type":"book-chapter","created":{"date-parts":[[2006,11,20]],"date-time":"2006-11-20T12:40:51Z","timestamp":1164026451000},"page":"529-548","source":"Crossref","is-referenced-by-count":2,"title":["Assume-Guarantee Software Verification Based on Game Semantics"],"prefix":"10.1007","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","reference":[{"key":"29_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"421","DOI":"10.1007\/978-3-540-24730-2_32","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Abramsky","year":"2004","unstructured":"Abramsky, S., Ghica, D.R., Murawski, A.S., Ong, C.-H.L.: Applying Game Semantics to Compositional Software Modeling and Verification. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 421\u2013435. Springer, Heidelberg (2004)"},{"key":"29_CR2","doi-asserted-by":"crossref","unstructured":"Abramsky, S., Jagadeesan, R., Malacaria, P.: Full Abstraction for PCF. Information and Computation\u00a0163(2) (2000)","DOI":"10.1006\/inco.2000.2930"},{"key":"29_CR3","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. Birkha\u00fcser, Basel (1997)","DOI":"10.1007\/978-1-4757-3851-3_10"},{"key":"29_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"548","DOI":"10.1007\/11513988_52","volume-title":"Computer Aided Verification","author":"R. Alur","year":"2005","unstructured":"Alur, R., Madhusudan, P., Nam, W.: Symbolic Compositional Verification by Learning Assumptions. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 548\u2013562. Springer, Heidelberg (2005)"},{"issue":"2","key":"29_CR5","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0890-5401(87)90052-6","volume":"75","author":"D. Angluin","year":"1987","unstructured":"Angluin, D.: Learning Regular Sets from Queries and Counterexamples. Information and Computation\u00a075(2), 87\u2013106 (1987)","journal-title":"Information and Computation"},{"key":"29_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/3-540-45139-0_7","volume-title":"Model Checking Software","author":"T. Ball","year":"2001","unstructured":"Ball, T., Rajamani, S.K.: Automatically Validating Temporal Safety Properties of Interfaces. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol.\u00a02057, pp. 103\u2013122. Springer, Heidelberg (2001)"},{"key":"29_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/11526841_34","volume-title":"FM 2005: Formal Methods","author":"S. Chaki","year":"2005","unstructured":"Chaki, S., Clarke, E., Sharygina, N., Sinha, N.: Dynamic Component Substiutability Analysis. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol.\u00a03582, pp. 512\u2013528. Springer, Heidelberg (2005)"},{"key":"29_CR8","volume-title":"Model Checking","author":"E.M. Clarke","year":"2000","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)"},{"key":"29_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/3-540-36577-X_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J.M. Cobleigh","year":"2003","unstructured":"Cobleigh, J.M., Giannakopoulou, D., Pasareanu, C.S.: Learning Assumptions for Compositional Verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 331\u2013346. Springer, Heidelberg (2003)"},{"key":"29_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-540-30482-1_18","volume-title":"Formal Methods and Software Engineering","author":"A. Dimovski","year":"2004","unstructured":"Dimovski, A., Lazic, R.: CSP Representation of Game Semantics for Second-Order Idealized Algol. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol.\u00a03308, pp. 146\u2013161. Springer, Heidelberg (2004)"},{"key":"29_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/11547662_9","volume-title":"Static Analysis","author":"A. Dimovski","year":"2005","unstructured":"Dimovski, A., Ghica, D.R., Lazic, R.: Data-Abstraction Refinement: A Game Semantic Approach. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol.\u00a03672, pp. 102\u2013117. Springer, Heidelberg (2005)"},{"key":"29_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1007\/11691617_17","volume-title":"Model Checking Software","author":"A. Dimovski","year":"2006","unstructured":"Dimovski, A., Ghica, D.R., Lazic, R.: A Counterexample-Guided Refinement Tool for Open Procedural Programs. In: Valmari, A. (ed.) SPIN 2006. LNCS, vol.\u00a03925, pp. 288\u2013292. Springer, Heidelberg (2006)"},{"key":"29_CR13","unstructured":"Formal Systems (Europe) Ltd Failures-Divergence Refinement: FDR2 Manual (2000), http:\/\/www.fsel.com"},{"issue":"1\u20133","key":"29_CR14","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1016\/S0304-3975(03)00315-3","volume":"309","author":"D.R. Ghica","year":"2003","unstructured":"Ghica, D.R., McCusker, G.: The Regular-Language Semantics of Second-order Idealized Algol. Theoretical Computer Science\u00a0309(1\u20133), 469\u2013502 (2003)","journal-title":"Theoretical Computer Science"},{"key":"29_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/3-540-46002-0_25","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Groce","year":"2002","unstructured":"Groce, A., Peled, D., Yannakakis, M.: Adaptive Model Checking. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol.\u00a02280, pp. 357\u2013370. Springer, Heidelberg (2002)"},{"key":"29_CR16","unstructured":"Harmer, R.: Games and Full Abstraction for Nondeterministic Languages. PhD thesis, Imperial College (1999)"},{"key":"29_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/3-540-44829-2_17","volume-title":"Model Checking Software","author":"T.A. Henzinger","year":"2003","unstructured":"Henzinger, T.A., Jhala, R., Majumdar, R., Sutre, G.: Software Verification with BLAST. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol.\u00a02648, pp. 235\u2013239. Springer, Heidelberg (2003)"},{"key":"29_CR18","doi-asserted-by":"publisher","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.: On Full Abstraction for PCF: I, II, and III. Information and Computation\u00a0163, 285\u2013400 (2000)","journal-title":"Information and Computation"},{"key":"29_CR19","doi-asserted-by":"crossref","unstructured":"Laird, J.: A Fully Abstract Game Semantics of Local Exceptions. In: Proceedings of LICS, pp. 105\u2013114 (2001)","DOI":"10.1109\/LICS.2001.932487"},{"key":"29_CR20","first-page":"123","volume":"13","author":"A. Pnueli","year":"1984","unstructured":"Pnueli, A.: In Transition from Global to Modular Temporal Reasoning about Programs. Logic and Models of Concurrent Systems\u00a013, 123\u2013144 (1984)","journal-title":"Logic and Models of Concurrent Systems"},{"issue":"2","key":"29_CR21","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1006\/inco.1993.1021","volume":"103","author":"R.L. Rivest","year":"1993","unstructured":"Rivest, R.L., Schapire, R.E.: Inference of finite automata using homing sequences. Information and Computation\u00a0103(2), 299\u2013347 (1993)","journal-title":"Information and Computation"},{"key":"29_CR22","volume-title":"Theory and Practice of Concurrency","author":"A.W. Roscoe","year":"1998","unstructured":"Roscoe, A.W.: Theory and Practice of Concurrency. Prentice-Hall, Englewood Cliffs (1998)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods and Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11901433_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,12]],"date-time":"2025-01-12T00:26:00Z","timestamp":1736641560000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11901433_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540474609","9783540474623"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/11901433_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2006]]}}}