{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,7,8]],"date-time":"2024-07-08T11:23:40Z","timestamp":1720437820256},"reference-count":54,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2014,10,1]],"date-time":"2014-10-01T00:00:00Z","timestamp":1412121600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2018,10,15]],"date-time":"2018-10-15T00:00:00Z","timestamp":1539561600000},"content-version":"vor","delay-in-days":1475,"URL":"https:\/\/2.zoppoz.workers.dev:443\/http\/www.elsevier.com\/open-access\/userlicense\/1.0\/"}],"funder":[{"name":"EU","award":["FP7-231620 HATS"],"award-info":[{"award-number":["FP7-231620 HATS"]}]}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Science of Computer Programming"],"published-print":{"date-parts":[[2014,10]]},"DOI":"10.1016\/j.scico.2013.10.002","type":"journal-article","created":{"date-parts":[[2013,10,26]],"date-time":"2013-10-26T08:16:10Z","timestamp":1382775370000},"page":"129-161","update-policy":"https:\/\/2.zoppoz.workers.dev:443\/http\/dx.doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":5,"special_numbering":"PB","title":["A fully abstract trace-based semantics for reasoning about backward compatibility of class libraries"],"prefix":"10.1016","volume":"92","author":[{"given":"Yannick","family":"Welsch","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arnd","family":"Poetzsch-Heffter","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"78","reference":[{"key":"10.1016\/j.scico.2013.10.002_br0010","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1002\/smr.328","article-title":"How do APIs evolve? A story of refactoring","author":"Dig","year":"2006","journal-title":"J. Softw. Maint. Evol."},{"key":"10.1016\/j.scico.2013.10.002_br0020","author":"des Rivi\u00e8res"},{"key":"10.1016\/j.scico.2013.10.002_br0040","series-title":"DAC","isbn-type":"print","doi-asserted-by":"crossref","first-page":"466","DOI":"10.1145\/1629911.1630034","article-title":"Regression verification","author":"Godlin","year":"2009","ISBN":"https:\/\/2.zoppoz.workers.dev:443\/http\/id.crossref.org\/isbn\/9781605584973"},{"issue":"1","key":"10.1016\/j.scico.2013.10.002_br0050","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1016\/0304-3975(77)90053-6","article-title":"Fully abstract models of typed lambda-calculi","volume":"4","author":"Milner","year":"1977","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"10.1016\/j.scico.2013.10.002_br0060","doi-asserted-by":"crossref","first-page":"223","DOI":"10.1016\/0304-3975(77)90044-5","article-title":"LCF considered as a programming language","volume":"5","author":"Plotkin","year":"1977","journal-title":"Theor. Comput. Sci."},{"key":"10.1016\/j.scico.2013.10.002_br0070","series-title":"ECOOP","isbn-type":"print","doi-asserted-by":"crossref","first-page":"412","DOI":"10.1007\/978-3-540-70592-5_18","article-title":"A unified framework for verification techniques for object invariants","volume":"vol. 5142","author":"Drossopoulou","year":"2008","ISBN":"https:\/\/2.zoppoz.workers.dev:443\/http\/id.crossref.org\/isbn\/9783540705918"},{"key":"10.1016\/j.scico.2013.10.002_br0080","series-title":"Object-Oriented Software Construction","author":"Meyer","year":"1997"},{"issue":"3","key":"10.1016\/j.scico.2013.10.002_br0090","doi-asserted-by":"crossref","first-page":"253","DOI":"10.1016\/j.scico.2006.03.001","article-title":"Modular invariants for layered object structures","volume":"62","author":"M\u00fcller","year":"2006","journal-title":"Sci. Comput. Program."},{"key":"10.1016\/j.scico.2013.10.002_br0100","series-title":"Formal Syntax and Semantics of Java","isbn-type":"print","first-page":"241","article-title":"A programmer's reduction semantics for classes and mixins","volume":"vol. 1523","author":"Flatt","year":"1999","ISBN":"https:\/\/2.zoppoz.workers.dev:443\/http\/id.crossref.org\/isbn\/3540661581"},{"key":"10.1016\/j.scico.2013.10.002_br0110","series-title":"ESOP","isbn-type":"print","first-page":"423","article-title":"Java Jr.: fully abstract trace semantics for a core Java language","volume":"vol. 3444","author":"Jeffrey","year":"2005","ISBN":"https:\/\/2.zoppoz.workers.dev:443\/http\/id.crossref.org\/isbn\/3540254358"},{"key":"10.1016\/j.scico.2013.10.002_br0120","series-title":"Informal Workshop Record of FOOL","article-title":"Reasoning about class behavior","author":"Koutavas","year":"2007"},{"key":"10.1016\/j.scico.2013.10.002_br0130","series-title":"OOPSLA","isbn-type":"print","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1145\/504282.504300","article-title":"Encapsulating objects with confined types","author":"Grothoff","year":"2001","ISBN":"https:\/\/2.zoppoz.workers.dev:443\/http\/id.crossref.org\/isbn\/1581133359"},{"key":"10.1016\/j.scico.2013.10.002_br0140","series-title":"Source compatibility for Java packages","author":"Welsch","year":"2010"},{"issue":"6","key":"10.1016\/j.scico.2013.10.002_br0150","doi-asserted-by":"crossref","first-page":"894","DOI":"10.1145\/1101821.1101824","article-title":"Ownership confinement ensures representation independence for object-oriented programs","volume":"52","author":"Banerjee","year":"2005","journal-title":"J. ACM"},{"key":"10.1016\/j.scico.2013.10.002_br0160","series-title":"ICTAC","isbn-type":"print","first-page":"37","article-title":"Object connectivity and full abstraction for a concurrent calculus of classes","volume":"vol. 3407","author":"\u00c1brah\u00e1m","year":"2004","ISBN":"https:\/\/2.zoppoz.workers.dev:443\/http\/id.crossref.org\/isbn\/3540253041"},{"key":"10.1016\/j.scico.2013.10.002_br0170","series-title":"SBMF","isbn-type":"print","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1007\/978-3-642-25032-3_3","article-title":"Full abstraction at package boundaries of object-oriented languages","volume":"vol. 7021","author":"Welsch","year":"2011","ISBN":"https:\/\/2.zoppoz.workers.dev:443\/http\/id.crossref.org\/isbn\/9783642250316"},{"key":"10.1016\/j.scico.2013.10.002_br0180","article-title":"The Java Language Specification","author":"Gosling","year":"2005"},{"key":"10.1016\/j.scico.2013.10.002_br0190","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1007\/s11784-012-0071-6","article-title":"How to write a 21st century proof","volume":"11","author":"Lamport","year":"2012","journal-title":"J. Fixed Point Theory Appl.","ISSN":"https:\/\/2.zoppoz.workers.dev:443\/http\/id.crossref.org\/issn\/1661-7738","issn-type":"print"},{"key":"10.1016\/j.scico.2013.10.002_br0200","author":"ECMA"},{"key":"10.1016\/j.scico.2013.10.002_br0210","series-title":"SAC","isbn-type":"print","doi-asserted-by":"crossref","first-page":"1737","DOI":"10.1145\/2245276.2232058","article-title":"A type system for checking specialization of packages in object-oriented programming","author":"Damiani","year":"2012","ISBN":"https:\/\/2.zoppoz.workers.dev:443\/http\/id.crossref.org\/isbn\/9781450308571"},{"issue":"3","key":"10.1016\/j.scico.2013.10.002_br0220","doi-asserted-by":"crossref","first-page":"396","DOI":"10.1145\/503502.503505","article-title":"Featherweight Java: a minimal core calculus for Java and GJ","volume":"23","author":"Igarashi","year":"2001","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"1","key":"10.1016\/j.scico.2013.10.002_br0230","doi-asserted-by":"crossref","first-page":"38","DOI":"10.1006\/inco.1994.1093","article-title":"A syntactic approach to type soundness","volume":"115","author":"Wright","year":"1994","journal-title":"Inf. Comput."},{"key":"10.1016\/j.scico.2013.10.002_br0240","series-title":"Lambda-calculus models of programming languages","author":"Morris","year":"1968"},{"key":"10.1016\/j.scico.2013.10.002_br0250","isbn-type":"print","article-title":"Algebraic Theory of Processes","author":"Hennessy","year":"1988","ISBN":"https:\/\/2.zoppoz.workers.dev:443\/http\/id.crossref.org\/isbn\/9780262081719"},{"key":"10.1016\/j.scico.2013.10.002_br0260","series-title":"Object-Connectivity and Observability for Class-Based, Object-Oriented Languages","author":"Steffen","year":"2006"},{"issue":"1\u20133","key":"10.1016\/j.scico.2013.10.002_br0270","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1016\/j.tcs.2004.10.012","article-title":"A fully abstract may testing semantics for concurrent objects","volume":"338","author":"Jeffrey","year":"2005","journal-title":"Theor. Comput. Sci."},{"key":"10.1016\/j.scico.2013.10.002_br0280","series-title":"Using Z \u2014 Specification, Refinement, and Proof","isbn-type":"print","author":"Woodcock","year":"1996","ISBN":"https:\/\/2.zoppoz.workers.dev:443\/http\/id.crossref.org\/isbn\/0139484728"},{"key":"10.1016\/j.scico.2013.10.002_br0290","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1007\/BF00289507","article-title":"Proof of correctness of data representations","volume":"1","author":"Hoare","year":"1972","journal-title":"Acta Inform."},{"key":"10.1016\/j.scico.2013.10.002_br0300","isbn-type":"print","article-title":"Programming from Specifications","author":"Morgan","year":"1994","ISBN":"https:\/\/2.zoppoz.workers.dev:443\/http\/id.crossref.org\/isbn\/9780131232747"},{"key":"10.1016\/j.scico.2013.10.002_br0310","series-title":"Refinement Calculus: A Systematic Introduction","author":"Back","year":"1998"},{"key":"10.1016\/j.scico.2013.10.002_br0320","series-title":"International Workshop on Aliasing, Confinement and Ownership","article-title":"Modular checking of confinement for object-oriented components using abstract interpretation","author":"Geilmann","year":"2011"},{"key":"10.1016\/j.scico.2013.10.002_br0330","series-title":"ICALP (2)","isbn-type":"print","doi-asserted-by":"crossref","first-page":"453","DOI":"10.1007\/978-3-642-22012-8_36","article-title":"Liveness-preserving atomicity abstraction","volume":"vol. 6756","author":"Gotsman","year":"2011","ISBN":"https:\/\/2.zoppoz.workers.dev:443\/http\/id.crossref.org\/isbn\/9783642220111"},{"issue":"51\u201352","key":"10.1016\/j.scico.2013.10.002_br0340","doi-asserted-by":"crossref","first-page":"4379","DOI":"10.1016\/j.tcs.2010.09.021","article-title":"Abstraction for concurrent objects","volume":"411","author":"Filipovic","year":"2010","journal-title":"Theor. Comput. Sci."},{"key":"10.1016\/j.scico.2013.10.002_br0350","series-title":"A denotational semantics of inheritance","author":"Cook","year":"1989"},{"key":"10.1016\/j.scico.2013.10.002_br0360","doi-asserted-by":"crossref","first-page":"60","DOI":"10.1016\/j.tcs.2012.02.009","article-title":"Refactoring and representation independence for class hierarchies","volume":"433","author":"Naumann","year":"2012","journal-title":"Theor. Comput. Sci."},{"key":"10.1016\/j.scico.2013.10.002_br0370","series-title":"ECOOP","isbn-type":"print","first-page":"387","article-title":"State based ownership, reentrance, and encapsulation","volume":"vol. 3586","author":"Banerjee","year":"2005","ISBN":"https:\/\/2.zoppoz.workers.dev:443\/http\/id.crossref.org\/isbn\/354027992X"},{"key":"10.1016\/j.scico.2013.10.002_br0380","series-title":"ECOOP","isbn-type":"print","first-page":"491","article-title":"Object invariants in dynamic contexts","volume":"vol. 3086","author":"Leino","year":"2004","ISBN":"https:\/\/2.zoppoz.workers.dev:443\/http\/id.crossref.org\/isbn\/354022159X"},{"key":"10.1016\/j.scico.2013.10.002_br0390","series-title":"OOPSLA","isbn-type":"print","doi-asserted-by":"crossref","first-page":"48","DOI":"10.1145\/286936.286947","article-title":"Ownership types for flexible alias protection","author":"Clarke","year":"1998","ISBN":"https:\/\/2.zoppoz.workers.dev:443\/http\/id.crossref.org\/isbn\/1581130058"},{"key":"10.1016\/j.scico.2013.10.002_br0400","series-title":"FME","isbn-type":"print","first-page":"82","article-title":"Class refinement and interface refinement in object-oriented programs","volume":"vol. 1313","author":"Mikhajlova","year":"1997","ISBN":"https:\/\/2.zoppoz.workers.dev:443\/http\/id.crossref.org\/isbn\/3540635335"},{"issue":"1","key":"10.1016\/j.scico.2013.10.002_br0410","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1007\/s001650070034","article-title":"Class refinement as semantics of correct object substitutability","volume":"12","author":"Back","year":"2000","journal-title":"Form. Asp. Comput."},{"issue":"5","key":"10.1016\/j.scico.2013.10.002_br0420","doi-asserted-by":"crossref","first-page":"547","DOI":"10.1007\/s00165-009-0125-8","article-title":"Blaming the client: on data refinement in the presence of pointers","volume":"22","author":"Filipovic","year":"2010","journal-title":"Form. Asp. Comput."},{"issue":"4\u20136","key":"10.1016\/j.scico.2013.10.002_br0430","doi-asserted-by":"crossref","first-page":"519","DOI":"10.1007\/s00165-012-0254-3","article-title":"Stepwise refinement of heap-manipulating code in Chalice","volume":"24","author":"Leino","year":"2012","journal-title":"Form. Asp. Comput."},{"key":"10.1016\/j.scico.2013.10.002_br0440","series-title":"ICALP","isbn-type":"print","first-page":"299","article-title":"On observing nondeterminism and concurrency","volume":"vol. 85","author":"Hennessy","year":"1980","ISBN":"https:\/\/2.zoppoz.workers.dev:443\/http\/id.crossref.org\/isbn\/3540100032"},{"issue":"1\u20133","key":"10.1016\/j.scico.2013.10.002_br0450","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1016\/j.tcs.2006.12.032","article-title":"A bisimulation for dynamic sealing","volume":"375","author":"Sumii","year":"2007","journal-title":"Theor. Comput. Sci."},{"issue":"5","key":"10.1016\/j.scico.2013.10.002_br0460","doi-asserted-by":"crossref","DOI":"10.1145\/1284320.1284325","article-title":"A bisimulation for type abstraction and recursion","volume":"54","author":"Sumii","year":"2007","journal-title":"J. ACM"},{"key":"10.1016\/j.scico.2013.10.002_br0470","series-title":"ESOP","isbn-type":"print","first-page":"146","article-title":"Bisimulations for untyped imperative objects","volume":"vol. 3924","author":"Koutavas","year":"2006","ISBN":"https:\/\/2.zoppoz.workers.dev:443\/http\/id.crossref.org\/isbn\/354033095X"},{"key":"10.1016\/j.scico.2013.10.002_br0480","series-title":"LICS","first-page":"293","article-title":"Environmental bisimulations for higher-order languages","author":"Sangiorgi","year":"2007"},{"key":"10.1016\/j.scico.2013.10.002_br0490","series-title":"Verification: Theory and Practice","isbn-type":"print","first-page":"11","article-title":"A logic of object-oriented programs","volume":"vol. 2772","author":"Abadi","year":"2003","ISBN":"https:\/\/2.zoppoz.workers.dev:443\/http\/id.crossref.org\/isbn\/3540210024"},{"key":"10.1016\/j.scico.2013.10.002_br0500","series-title":"ESOP","isbn-type":"print","first-page":"162","article-title":"A programming logic for sequential Java","volume":"vol. 1576","author":"Poetzsch-Heffter","year":"1999","ISBN":"https:\/\/2.zoppoz.workers.dev:443\/http\/id.crossref.org\/isbn\/3540656995"},{"key":"10.1016\/j.scico.2013.10.002_br0510","series-title":"Proceedings of the 14th Workshop on Formal Techniques for Java-Like Programs, FTfJP '12","first-page":"35","article-title":"Verifying backwards compatibility of object-oriented libraries using boogie","author":"Welsch","year":"2012"},{"key":"10.1016\/j.scico.2013.10.002_br0520","series-title":"FMCO","isbn-type":"print","first-page":"364","article-title":"Boogie: a modular reusable verifier for object-oriented programs","volume":"vol. 4111","author":"Barnett","year":"2005","ISBN":"https:\/\/2.zoppoz.workers.dev:443\/http\/id.crossref.org\/isbn\/3540367497"},{"key":"10.1016\/j.scico.2013.10.002_br0530","author":"Welsch"},{"key":"10.1016\/j.scico.2013.10.002_br0540","series-title":"ECOOP","isbn-type":"print","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1007\/978-3-642-14107-2_13","article-title":"JCoBox generalizing active objects to concurrent components","volume":"vol. 6183","author":"Sch\u00e4fer","year":"2010","ISBN":"https:\/\/2.zoppoz.workers.dev:443\/http\/id.crossref.org\/isbn\/9783642141065"},{"key":"10.1016\/j.scico.2013.10.002_br0550","series-title":"FMCO","isbn-type":"print","doi-asserted-by":"crossref","first-page":"142","DOI":"10.1007\/978-3-642-25271-6_8","article-title":"ABS: a core language for abstract behavioral specification","volume":"vol. 6957","author":"Johnsen","year":"2010","ISBN":"https:\/\/2.zoppoz.workers.dev:443\/http\/id.crossref.org\/isbn\/9783642252709"}],"container-title":["Science of Computer Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/api.elsevier.com\/content\/article\/PII:S0167642313002529?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/api.elsevier.com\/content\/article\/PII:S0167642313002529?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2023,7,5]],"date-time":"2023-07-05T16:57:50Z","timestamp":1688576270000},"score":1,"resource":{"primary":{"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/linkinghub.elsevier.com\/retrieve\/pii\/S0167642313002529"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,10]]},"references-count":54,"alternative-id":["S0167642313002529"],"URL":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1016\/j.scico.2013.10.002","relation":{},"ISSN":["0167-6423"],"issn-type":[{"value":"0167-6423","type":"print"}],"subject":[],"published":{"date-parts":[[2014,10]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"A fully abstract trace-based semantics for reasoning about backward compatibility of class libraries","name":"articletitle","label":"Article Title"},{"value":"Science of Computer Programming","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/2.zoppoz.workers.dev:443\/https\/doi.org\/10.1016\/j.scico.2013.10.002","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"Copyright \u00a9 2013 Elsevier B.V. All rights reserved.","name":"copyright","label":"Copyright"}]}}