{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,12]],"date-time":"2025-02-12T14:10:55Z","timestamp":1739369455774,"version":"3.37.0"},"reference-count":52,"publisher":"Association for Computing Machinery (ACM)","issue":"5","license":[{"start":{"date-parts":[[2010,9,1]],"date-time":"2010-09-01T00:00:00Z","timestamp":1283299200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2010,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Data refinement is a common approach to reasoning about programs, based on establishing that a concrete program indeed satisfies all the required properties imposed by an intended abstract pattern. Reasoning about programs in this setting becomes complex when use of pointers is assumed and, moreover, a well-known method for proving data refinement, namely the forward simulation method, becomes unsound in presence of pointers. The reason for unsoundness is the failure of the \u201clifting theorem\u201d for simulations: that a simulation between abstract and concrete modules can be lifted to all client programs. The result is that simulation does not imply that a concrete can replace an abstract module in all contexts. Our diagnosis of this problem is that unsoundness is due to interference from the client programs. Rather than blame a module for the unsoundness of lifting simulations, our analysis places the blame on the client programs which cause the interference: when interference is not present, soundness is recovered. Technically, we present a novel instrumented semantics which is capable of detecting interference between a module and its client. With use of special simulation relations, namely growing relations, and interpreting the simulation method using the instrumented semantics, we obtain a lifting theorem. We then show situations under which simulation does indeed imply refinement.<\/jats:p>","DOI":"10.1007\/s00165-009-0125-8","type":"journal-article","created":{"date-parts":[[2009,10,1]],"date-time":"2009-10-01T15:59:52Z","timestamp":1254412792000},"page":"547-583","source":"Crossref","is-referenced-by-count":13,"title":["Blaming the client: on data refinement in the presence of pointers"],"prefix":"10.1145","volume":"22","author":[{"given":"Ivana","family":"Filipovi\u0107","sequence":"first","affiliation":[{"name":"Queen Mary, University of London, Mile End Road, E1 4NS, London, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"O\u2019Hearn","sequence":"additional","affiliation":[{"name":"Queen Mary, University of London, Mile End Road, E1 4NS, London, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Noah","family":"Torp-Smith","sequence":"additional","affiliation":[{"name":"Maconomy A\/S, Vordingborggade 18-22, 2100, Copenhagen, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hongseok","family":"Yang","sequence":"additional","affiliation":[{"name":"Queen Mary, University of London, Mile End Road, E1 4NS, London, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","unstructured":"Back RJ (1978) On the correctness of refinement steps in program development. Technical Report A-1978-4 Department of Computer Science University of Helsinki"},{"volume-title":"Correctness preserving program refinements: proof theory and applications. Volume 131 of Mathematical Centre Tracts","year":"1980","author":"Back RJ","key":"e_1_2_1_2_2_2"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Biering B Birkedal L Torp-Smith N (2007) BI-hyperdoctrines higher-order separation logic and abstraction. ACM Trans Program Lang Syst 29(5)","DOI":"10.1145\/1275497.1275499"},{"key":"e_1_2_1_2_4_2","doi-asserted-by":"crossref","unstructured":"Barnett M DeLine R F\u00e4hndrich M Rustan K Leino M Schulte W (2004) Verification of object-oriented programs with invariants. JOT 3(6)","DOI":"10.5381\/jot.2004.3.6.a2"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Benton N (2006) Abstracting allocation: the new new thing. In: Proceedings of computer science logic (CSL\u201906) volume 4207 of LNCS","DOI":"10.1007\/11874683_12"},{"key":"e_1_2_1_2_6_2","unstructured":"Back RJ Fan X Preoteasa V (2003) Reasoning about pointers in refinement calculus. In Proceedings of the tenth Asia-Pacific software engineering conference (APSEC\u201903)"},{"key":"e_1_2_1_2_7_2","doi-asserted-by":"crossref","unstructured":"Benton N Leperchley B (2005) Relational reasoning in a nominal semantics for storage. In: 7th TLCA LNCS 3641 pp 86\u2013101","DOI":"10.1007\/11417170_8"},{"key":"e_1_2_1_2_8_2","doi-asserted-by":"publisher","DOI":"10.1145\/1101821.1101824"},{"key":"e_1_2_1_2_9_2","doi-asserted-by":"crossref","unstructured":"Banerjee A Naumann D (2005) State based ownership reentrance and encapsulation. In: Proceedings of the nineteenth European conference on object-oriented programming (ECOOP) volume 3586 of LNCS. Springer-Verlag pp 387 \u2013411","DOI":"10.1007\/11531142_17"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"crossref","unstructured":"Banerjee A Naumann D Rosenberg S (2008) Regional logic for local reasoning about global invariants. In: Proceedings of the 22nd European conference on object-oriented programming (ECOOP) volume 5142 of LNCS. Springer-Verlag pp 387\u2013411","DOI":"10.1007\/978-3-540-70592-5_17"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Bornat R (2000) Proving pointer programs in Hoare logic. In: Mathematics of program construction","DOI":"10.1007\/10722010_8"},{"key":"e_1_2_1_2_12_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.034"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(98)00016-1"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Birkedal L Yang H (2007) Relational parametricity and separation logic. In: 10th FOSSACS","DOI":"10.2168\/LMCS-4(2:6)2008"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"Clarke DG Noble J Potter JM (2001) Simple ownership types for object containment. In: Proceedings of European conference on object-oriented programming","DOI":"10.1007\/3-540-45337-7_4"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"de Roever W-P Engelhardt K (1998) Data Refinement: Model-Oriented Proof Methods and their Comparison. Number 47 in Cambridge tracts in theoretical computer science. Cambridge University Press Cambridge UK","DOI":"10.1017\/CBO9780511663079"},{"key":"e_1_2_1_2_17_2","doi-asserted-by":"crossref","unstructured":"Foster JC Osipov V Bhalla N (2005) Buffer overflow attacks: detect exploit prevent. Syngress Publishing Inc.","DOI":"10.1016\/B978-193226667-2\/50037-2"},{"key":"e_1_2_1_2_18_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(91)90029-2"},{"key":"e_1_2_1_2_19_2","unstructured":"Hoare CAR He J (1990) Data refinement in a categorical setting. Technical Report PRG-90 Oxford University Computing Laboratory"},{"key":"e_1_2_1_2_20_2","doi-asserted-by":"crossref","unstructured":"He J Hoare CAR Sanders JW (1986) Data refinement refined (resume). In: Robinet B Wilhelm R (eds) ESOP 86 European symposium on programming volume 213 of Lecture notes in computer science. Springer Verlag pp 187\u2013196","DOI":"10.1007\/3-540-16442-1_14"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00289507"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Hogg J (1991) Islands: aliasing protection in object-oriented languages. In: OOPSLA\u201991","DOI":"10.1145\/117954.117975"},{"key":"e_1_2_1_2_23_2","doi-asserted-by":"crossref","unstructured":"Ishtiaq S O\u2019Hearn PW (2001) BI as an assertion language for mutable data structures. In: Principles of programming languages vol 28. ACM - SIGPLAN London","DOI":"10.1145\/360204.375719"},{"key":"e_1_2_1_2_24_2","unstructured":"Jones CB (1980) Software development: a rigorous approach. Prentice-Hall"},{"key":"e_1_2_1_2_25_2","unstructured":"Advanced Doug Lea\u2019s malloc exploits (2001) Internet page 2001. Avaiable at http:\/\/doc.bughunter.net\/buffer-overflow\/advanced-malloc-exploits.html"},{"key":"e_1_2_1_2_26_2","unstructured":"Michel \u201cMaXX\u201d Kaempf (2001) Smashing the heap for fun and profit. Internet page 2001. Available at http:\/\/doc.bughunter.net\/buffer-overflow\/heap-corruption.html#gnu_malloc"},{"key":"e_1_2_1_2_27_2","unstructured":"Knuth DE (1973) The art of computer programming Volume I: fundamental algorithms 2nd edn. Addison-Wesley"},{"key":"e_1_2_1_2_28_2","doi-asserted-by":"publisher","DOI":"10.5555\/576122"},{"key":"e_1_2_1_2_29_2","unstructured":"Lea D (2001) A memory allocator. Internet page. Avaiable at http:\/\/g.oswego.edu\/dl\/html\/malloc.html"},{"key":"e_1_2_1_2_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-007-0026-7"},{"key":"e_1_2_1_2_31_2","unstructured":"Mijajlovi\u0107 I (2007) Separation and data refinement. PhD thesis Queen Mary University of London"},{"key":"e_1_2_1_2_32_2","unstructured":"Morgan C Robinson K Gardiner P (1988) On the refinement calculus. Technical Report PRG-70 Oxford University Computing Laboratory October 1988"},{"key":"e_1_2_1_2_33_2","doi-asserted-by":"crossref","unstructured":"Mijajlovi\u0107 I Torp-Smith N O\u2019Hearn P (2004) Refinement and separation contexts. In: Lodaya K Mahajan M (eds) STTCS volume LNCS 3328 pp 421\u2013433","DOI":"10.1007\/978-3-540-30538-5_35"},{"key":"e_1_2_1_2_34_2","doi-asserted-by":"crossref","unstructured":"Mijajlovi\u0107 I Yang H (2005) Data refinement with low-level pointer operations. In: Yi K (ed) Programming languages and systems volume LNCS 3780 pp 19\u201336","DOI":"10.1007\/11575467_3"},{"key":"e_1_2_1_2_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-006-0020-5"},{"key":"e_1_2_1_2_36_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_2_1_2_37_2","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn P Pym DJ (1999) The logic of bunched implications. Bull Symbolic Logic 5(2)","DOI":"10.2307\/421090"},{"key":"e_1_2_1_2_38_2","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn PW Reynolds JC Yang H (2001) Local reasoning about programs that alter data structures. In: Proceedings of 15th annual conference of the European association for computer science logic: CSL 2001 Lecture notes in computer science Berlin Springer-Verlag","DOI":"10.1007\/3-540-44802-0_1"},{"issue":"3","key":"e_1_2_1_2_39_2","first-page":"50","article-title":"Separation and information hiding","volume":"31","author":"O\u2019Hearn P","year":"2009","journal-title":"ACM TOPLAS"},{"key":"e_1_2_1_2_40_2","unstructured":"Parkinson M (2007) Class invariants: the end of the road? Position paper presented at 3rd international workshop on aliasing confinement and ownership in object-oriented programming"},{"key":"e_1_2_1_2_41_2","doi-asserted-by":"crossref","unstructured":"Parkinson M Bierman G (2005) Separation logic and abstraction. In: 32nd POPL pp 59\u201370","DOI":"10.1145\/1040305.1040326"},{"key":"e_1_2_1_2_42_2","unstructured":"Plotkin GD (1973) Lambda definability and logical relations. Technical Report SAI-RM-4 School of Artificial Intelligence University of Edinburgh"},{"key":"e_1_2_1_2_43_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.11.020"},{"key":"e_1_2_1_2_44_2","unstructured":"Reynolds JC (1983) Types abstraction and parametric polymorphism. In: Proceedings of IFIP congress"},{"key":"e_1_2_1_2_45_2","doi-asserted-by":"crossref","unstructured":"Reynolds JC (2002) Separation logic: a logic for shared mutable data structures. In: Proceedings of logic in computer science vol 17 pp 55 \u2013 74 Copenhagen July 2002. IEEE","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_1_2_46_2","unstructured":"Reynolds JC (2005) Precise intuitionistic and supported assertions in separation logic May 2005. Slides from the invited talk given at the MFPS XXI Available at author\u2019s home page: http:\/\/www.cs.cmu.edu\/~jcr\/"},{"key":"#cr-split#-e_1_2_1_2_47_2.1","doi-asserted-by":"crossref","unstructured":"Reddy US Yang H (2003) Correctness of data representations involving heap data structures. In: Degano P","DOI":"10.1007\/3-540-36575-3_16"},{"key":"#cr-split#-e_1_2_1_2_47_2.2","unstructured":"(ed) Proceedings of the 12th European symposium on programming ESOP 2003 Springer Verlag pp 223-237"},{"issue":"2","key":"e_1_2_1_2_48_2","doi-asserted-by":"crossref","first-page":"151","DOI":"10.1093\/comjnl\/20.2.151","article-title":"Generic commands\u2014a tool for partial correctness formalisms","volume":"10","author":"Schwarz J","year":"1977","journal-title":"Comput J"},{"key":"e_1_2_1_2_49_2","unstructured":"Yang H (2001) Local reasoning for stateful programs. PhD thesis University of Illinois"},{"key":"e_1_2_1_2_50_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.036"},{"key":"e_1_2_1_2_51_2","doi-asserted-by":"crossref","unstructured":"Yang H O\u2019Hearn P (2002) A semantic basis for local reasoning. In: Proceedings of FOSSACS","DOI":"10.1007\/3-540-45931-6_28"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-009-0125-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00165-009-0125-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-009-0125-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,2,12]],"date-time":"2025-02-12T13:56:33Z","timestamp":1739368593000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-009-0125-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,9]]},"references-count":52,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2010,9]]}},"alternative-id":["10.1007\/s00165-009-0125-8"],"URL":"https:\/\/doi.org\/10.1007\/s00165-009-0125-8","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2010,9]]}}}