{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,30]],"date-time":"2025-04-30T06:26:50Z","timestamp":1745994410814,"version":"3.40.3"},"publisher-location":"Singapore","reference-count":30,"publisher":"Springer Nature Singapore","isbn-type":[{"type":"print","value":"9789819983100"},{"type":"electronic","value":"9789819983117"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"DOI":"10.1007\/978-981-99-8311-7_13","type":"book-chapter","created":{"date-parts":[[2023,11,22]],"date-time":"2023-11-22T07:02:17Z","timestamp":1700636537000},"page":"269-289","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Incorrectness Proofs for\u00a0Object-Oriented Programs via\u00a0Subclass Reflection"],"prefix":"10.1007","author":[{"given":"Wenhua","family":"Li","sequence":"first","affiliation":[]},{"given":"Quang Loc","family":"Le","sequence":"additional","affiliation":[]},{"given":"Yahui","family":"Song","sequence":"additional","affiliation":[]},{"given":"Wei-Ngan","family":"Chin","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,11,21]]},"reference":[{"key":"13_CR1","unstructured":"Infer Static Analyzer: Infer. https:\/\/fbinfer.com\/. Accessed 02 June 2023"},{"key":"13_CR2","unstructured":"Pulse, an interprocedural memory safety analysis. https:\/\/github.com\/facebook\/infer\/tree\/main\/infer\/tests\/codetoanalyze\/java\/pulse. Accessed 20 May 2023"},{"issue":"6","key":"13_CR3","doi-asserted-by":"publisher","first-page":"27","DOI":"10.5381\/jot.2004.3.6.a2","volume":"3","author":"M Barnett","year":"2004","unstructured":"Barnett, M., DeLine, R., F\u00e4hndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. J. Object Technol. 3(6), 27\u201356 (2004)","journal-title":"J. Object Technol."},{"issue":"1","key":"13_CR4","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1145\/1328897.1328452","volume":"43","author":"W-N Chin","year":"2008","unstructured":"Chin, W.-N., David, C., Nguyen, H.H., Qin, S.: Enhancing modular OO verification with separation logic. ACM SIGPLAN Notices 43(1), 87\u201399 (2008)","journal-title":"ACM SIGPLAN Notices"},{"issue":"9","key":"13_CR5","doi-asserted-by":"publisher","first-page":"1006","DOI":"10.1016\/j.scico.2010.07.004","volume":"77","author":"W-N Chin","year":"2012","unstructured":"Chin, W.-N., David, C., Nguyen, H.H., Qin, S.: Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Sci. Comput. Prog. 77(9), 1006\u20131036 (2012)","journal-title":"Sci. Comput. Prog."},{"key":"13_CR6","doi-asserted-by":"crossref","unstructured":"Cook, W.R., Hill, W., Canning, P.S.: Inheritance is not subtyping. In: Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1990), New York, pp. 125\u2013135. Association for Computing Machinery (1989)","DOI":"10.1145\/96709.96721"},{"key":"13_CR7","doi-asserted-by":"crossref","unstructured":"Dhara, K.K., Leavens, G.T.: Forcing behavioral subtyping through specification inheritance. In: Proceedings of the 18th International Conference on Software Engineering (ICSE 1996), pp. 258\u2013267. IEEE Computer Society (1996)","DOI":"10.1109\/ICSE.1996.493421"},{"issue":"4","key":"13_CR8","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/BF00289507","volume":"1","author":"CAR Hoare","year":"1972","unstructured":"Hoare, C.A.R.: Proof of correctness of data representations. Acta Informatica 1(4), 271\u2013281 (1972)","journal-title":"Acta Informatica"},{"key":"13_CR9","doi-asserted-by":"publisher","unstructured":"Huisman, M., Jacobs, B.: Java program verification via a hoare logic with abrupt termination. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol. 1783, pp. 284\u2013303. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-46428-X_20","DOI":"10.1007\/3-540-46428-X_20"},{"key":"13_CR10","doi-asserted-by":"publisher","unstructured":"Kassios, I.T.: Dynamic frames: support for framing, dependencies and sharing without restrictions. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 268\u2013283. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11813040_19","DOI":"10.1007\/11813040_19"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"Le, Q.L., Raad, A., Villard, J., Berdine, J., Dreyer, D., O\u2019Hearn, P.W.: Finding real bugs in big programs with incorrectness logic. Proc. ACM Program. Lang. 6(OOPSLA1) (2022)","DOI":"10.1145\/3527325"},{"key":"13_CR12","doi-asserted-by":"publisher","unstructured":"Le, Q.L., Sun, J., Qin, S.: Frame inference for inductive entailment proofs in separation logic. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 41\u201360. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_3","DOI":"10.1007\/978-3-319-89960-2_3"},{"key":"13_CR13","doi-asserted-by":"crossref","unstructured":"Leavens, G.T., Naumann, D.A.: Behavioral subtyping, specification inheritance, and modular reasoning. ACM Trans. Prog. Lang. Syst. 37(4), 1\u201388 (2015)","DOI":"10.1145\/2766446"},{"key":"13_CR14","doi-asserted-by":"crossref","unstructured":"Leavens, G.T., Weihl, W.E.: Specification and verification of object-oriented programs using supertype abstraction. Acta Informatica 32(8), 705\u2013778 (1995)","DOI":"10.1007\/BF01178658"},{"key":"13_CR15","doi-asserted-by":"publisher","unstructured":"Leino, K.R.M., M\u00fcller, P.: Object invariants in dynamic contexts. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 491\u2013515. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24851-4_22","DOI":"10.1007\/978-3-540-24851-4_22"},{"key":"13_CR16","doi-asserted-by":"crossref","unstructured":"Li, W., Le, Q.L., Song, Y., Chin, W.-N.: Incorrectness proofs for object-oriented programs via subclass reflection (technical report). https:\/\/www.comp.nus.edu.sg\/~yahuis\/APLAS2023.pdf (2023)","DOI":"10.1007\/978-981-99-8311-7_13"},{"key":"13_CR17","doi-asserted-by":"crossref","unstructured":"Liskov, B.: Keynote address-data abstraction and hierarchy. In: Addendum to the Proceedings on Object-Oriented Programming Systems, Languages and Applications (Addendum), pp. 17\u201334 (1987)","DOI":"10.1145\/62138.62141"},{"issue":"6","key":"13_CR18","doi-asserted-by":"publisher","first-page":"1811","DOI":"10.1145\/197320.197383","volume":"16","author":"BH Liskov","year":"1994","unstructured":"Liskov, B.H., Wing, J.M.: A behavioral notion of subtyping. ACM Trans. Program. Lang. Syst. 16(6), 1811\u20131841 (1994)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"13_CR19","doi-asserted-by":"crossref","unstructured":"Long, F., Amidon, P., Rinard, M.: Automatic inference of code transforms for patch generation. In: Proceedings of the 2017 11th Joint Meeting on Foundations of Software Engineering, pp. 727\u2013739 (2017)","DOI":"10.1145\/3106237.3106253"},{"key":"13_CR20","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/j.entcs.2008.04.051","volume":"212","author":"C Luo","year":"2008","unstructured":"Luo, C., Qin, S.: Separation logic for multiple inheritance. Electron. Notes Theor. Comput. Sci. 212, 27\u201340 (2008)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"key":"13_CR21","doi-asserted-by":"crossref","unstructured":"Madeiral, F., Urli, S., Maia, M., Monperrus, M.: Bears: an extensible java bug benchmark for automatic program repair studies. In: 2019 IEEE 26th International Conference on Software Analysis, Evolution and Reengineering (SANER), pp. 468\u2013478. IEEE (2019)","DOI":"10.1109\/SANER.2019.8667991"},{"key":"13_CR22","doi-asserted-by":"publisher","unstructured":"O\u2019Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 1\u201319. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44802-0_1","DOI":"10.1007\/3-540-44802-0_1"},{"key":"13_CR23","doi-asserted-by":"crossref","unstructured":"O\u2019Hearn, P.W.: Incorrectness logic. Proc. ACM Prog. Lang. 4(POPL), 10:1\u201310:32 (2020)","DOI":"10.1145\/3371078"},{"key":"13_CR24","doi-asserted-by":"crossref","unstructured":"Parkinson, M., Bierman, G.: Separation logic and abstraction. In: Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 247\u2013258 (2005)","DOI":"10.1145\/1040305.1040326"},{"issue":"1","key":"13_CR25","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1145\/1328897.1328451","volume":"43","author":"MJ Parkinson","year":"2008","unstructured":"Parkinson, M.J., Bierman, G.M.: Separation logic, abstraction and inheritance. ACM SIGPLAN Notices 43(1), 75\u201386 (2008)","journal-title":"ACM SIGPLAN Notices"},{"key":"13_CR26","doi-asserted-by":"publisher","unstructured":"Raad, A., Berdine, J., Dang, H.-H., Dreyer, D., O\u2019Hearn, P., Villard, J.: Local reasoning about the presence of bugs: incorrectness separation Logic. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12225, pp. 225\u2013252. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53291-8_14","DOI":"10.1007\/978-3-030-53291-8_14"},{"issue":"4","key":"13_CR27","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1145\/3188720","volume":"61","author":"C Sadowski","year":"2018","unstructured":"Sadowski, C., Aftandilian, E., Eagle, A., Miller-Cushon, L., Jaspan, C.: Lessons from building static analysis tools at google. Commun. ACM 61(4), 58\u201366 (2018)","journal-title":"Commun. ACM"},{"key":"13_CR28","doi-asserted-by":"crossref","unstructured":"Tomassi, D.A., et al.: Bugswarm: mining and continuously growing a dataset of reproducible failures and fixes. In: 2019 IEEE\/ACM 41st International Conference on Software Engineering (ICSE), pp. 339\u2013349. IEEE (2019)","DOI":"10.1109\/ICSE.2019.00048"},{"key":"13_CR29","doi-asserted-by":"crossref","unstructured":"van Tonder, R., Le Goues, C.: Static automated program repair for heap properties. In: Proceedings of the 40th International Conference on Software Engineering, pp. 151\u2013162 (2018)","DOI":"10.1145\/3180155.3180250"},{"key":"13_CR30","doi-asserted-by":"publisher","unstructured":"de Vries, E., Koutavas, V.: Reverse hoare logic. In: Barthe, G., Pardo, A., Schneider, G. (eds.) SEFM 2011. LNCS, vol. 7041, pp. 155\u2013171. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24690-6_12","DOI":"10.1007\/978-3-642-24690-6_12"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-99-8311-7_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,2]],"date-time":"2024-11-02T16:26:28Z","timestamp":1730564788000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-99-8311-7_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9789819983100","9789819983117"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-981-99-8311-7_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"21 November 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"APLAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Asian Symposium on Programming Languages and Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Taipei","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Taiwan","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 November 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 November 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"aplas2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/home\/aplas-2023","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"HotCRP","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"32","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"15","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"47% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}