{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:40:11Z","timestamp":1750297211379,"version":"3.41.0"},"reference-count":25,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2025,3,3]],"date-time":"2025-03-03T00:00:00Z","timestamp":1740960000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2025,6,30]]},"abstract":"<jats:p>\n            We introduce a new way of reasoning about invariance in terms of\n            <jats:italic>footprints<\/jats:italic>\n            in a program logic for object-oriented components. A footprint of an object-oriented component is formalized as a monadic predicate that describes which objects on the heap can be affected by the execution of the component. Assuming encapsulation, this amounts to specifying which objects of the component can be called. Adaptation of local specifications into global specifications amounts to showing invariance of assertions, which is ensured by means of a form of\n            <jats:italic>bounded quantification<\/jats:italic>\n            which excludes references to a given footprint. The new approach is compared to two existing approaches to reason about invariance: separation logic and dynamic frames.\n          <\/jats:p>","DOI":"10.1145\/3703921","type":"journal-article","created":{"date-parts":[[2024,11,20]],"date-time":"2024-11-20T11:03:21Z","timestamp":1732100601000},"page":"1-23","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Footprint Logic for Object-Oriented Components (extended paper)"],"prefix":"10.1145","volume":"37","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3950-6271","authenticated-orcid":false,"given":"F. S.","family":"de Boer","sequence":"first","affiliation":[{"name":"Leiden Institute of Advanced Computer Science, Leiden University, Leiden, Netherlands and Centrum Wiskunde en Informatica, Amsterdam, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2964-6844","authenticated-orcid":false,"given":"Stijn","family":"de Gouw","sequence":"additional","affiliation":[{"name":"Open University of The Netherlands, Heerlen, Netherlands and Centrum Wiskunde en Informatica, Amsterdam, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9677-6644","authenticated-orcid":false,"given":"Hans-Dieter","family":"Hiep","sequence":"additional","affiliation":[{"name":"Centrum Wiskunde &amp; Informatica, Amsterdam, Netherlands and Leiden Institute of Advanced Computer Science, Leiden University, Leiden, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5003-598X","authenticated-orcid":false,"given":"Jinting","family":"Bian","sequence":"additional","affiliation":[{"name":"Leiden Institute of Advanced Computer Science, Leiden University, Leiden, Netherlands and Centrum Wiskunde en Informatica, Amsterdam, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,3,3]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-49812-6"},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.5555\/1642724"},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2011.08.002"},{"issue":"1","key":"e_1_3_3_5_2","first-page":"17","article-title":"Taclets: A new paradigm for constructing interactive theorem provers","volume":"98","author":"Beckert Bernhard","year":"2004","unstructured":"Bernhard Beckert, Martin Giese, Elmar Habermalz, Reiner H\u00e4hnle, Andreas Roth, and Steffen Schlager. 2004. Taclets: A new paradigm for constructing interactive theorem provers. RACSAM 98, 1 (2004), 17\u201353.","journal-title":"RACSAM"},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.6084\/m9.figshare.16782667.v1"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.6044345"},{"key":"e_1_3_3_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-66845-1_7"},{"key":"e_1_3_3_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45294-X_10"},{"key":"e_1_3_3_10_2","first-page":"135","volume-title":"Foundations of Software Science and Computation Structure, Second International Conference, FoSSaCS\u201999, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS\u201999, Amsterdam, The Netherlands, March 22-28, 1999, Proceedings","author":"Boer Frank S. de","year":"1999","unstructured":"Frank S. de Boer. 1999. A WP-calculus for OO. In Foundations of Software Science and Computation Structure, Second International Conference, FoSSaCS\u201999, Held as Part of the European Joint Conferences on the Theory and Practice of Software, ETAPS\u201999, Amsterdam, The Netherlands, March 22-28, 1999, Proceedings. 135\u2013149."},{"key":"e_1_3_3_11_2","first-page":"191","volume-title":"Correct System Design - Symposium in Honor of Ernst-R\u00fcdiger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 8-9, 2015. Proceedings","author":"Boer Frank S. de","year":"2015","unstructured":"Frank S. de Boer and Stijn de Gouw. 2015. Being and change: Reasoning about invariance. In Correct System Design - Symposium in Honor of Ernst-R\u00fcdiger Olderog on the Occasion of His 60th Birthday, Oldenburg, Germany, September 8-9, 2015. Proceedings. 191\u2013204."},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-20872-0_9"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-014-0446-9"},{"key":"e_1_3_3_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-49812-6_19"},{"key":"e_1_3_3_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/1449764.1449782"},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2016.04.004"},{"key":"e_1_3_3_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0059696"},{"key":"e_1_3_3_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/11813040_19"},{"key":"e_1_3_3_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-5229-1_12"},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(83)90009-9"},{"key":"e_1_3_3_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36946-9_13"},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_3_3_24_2","first-page":"460","volume-title":"Verified Software: Theories, Tools, Experiments, First IFIP TC 2\/WG 2.3 Conference, VSTTE 2005, Zurich, Switzerland, October 10-13, 2005, Revised Selected Papers and Discussions","author":"Reynolds John C.","year":"2005","unstructured":"John C. Reynolds. 2005. An overview of separation logic. In Verified Software: Theories, Tools, Experiments, First IFIP TC 2\/WG 2.3 Conference, VSTTE 2005, Zurich, Switzerland, October 10-13, 2005, Revised Selected Papers and Discussions. 460\u2013469."},{"key":"e_1_3_3_25_2","volume-title":"Deductive Verification of Object-Oriented Software: Dynamic Frames, Dynamic Logic and Predicate Abstraction","author":"Wei\u00df Benjamin","year":"2011","unstructured":"Benjamin Wei\u00df. 2011. Deductive Verification of Object-Oriented Software: Dynamic Frames, Dynamic Logic and Predicate Abstraction. Ph. D. Dissertation. Karlsruhe Institute of Technology."},{"key":"e_1_3_3_26_2","doi-asserted-by":"crossref","unstructured":"Job Zwiers Ulrich Hannemann Yassine Lakhnech Willem P. de Roever and Frank A. Stomp. 1996. Modular completeness: Integrating the reuse of specified software in top-down program development(Lecture Notes in Computer Science Vol. 1051) Marie-Claude Gaudel and Jim Woodcock (Eds.). Springer 595\u2013608.","DOI":"10.1007\/3-540-60973-3_109"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3703921","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3703921","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:18:06Z","timestamp":1750295886000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3703921"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,3,3]]},"references-count":25,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2025,6,30]]}},"alternative-id":["10.1145\/3703921"],"URL":"https:\/\/doi.org\/10.1145\/3703921","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2025,3,3]]},"assertion":[{"value":"2023-05-31","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-10-29","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-03","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}