{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T19:18:30Z","timestamp":1742930310712,"version":"3.40.3"},"publisher-location":"Cham","reference-count":15,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319307336"},{"type":"electronic","value":"9783319307343"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-30734-3_13","type":"book-chapter","created":{"date-parts":[[2016,3,12]],"date-time":"2016-03-12T08:19:52Z","timestamp":1457770792000},"page":"173-193","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A Sound and Complete Hoare Logic for Dynamically-Typed, Object-Oriented Programs"],"prefix":"10.1007","author":[{"given":"Bj\u00f6rn","family":"Engelmann","sequence":"first","affiliation":[]},{"given":"Ernst-R\u00fcdiger","family":"Olderog","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,3,13]]},"reference":[{"issue":"4","key":"13_CR1","doi-asserted-by":"publisher","first-page":"431","DOI":"10.1145\/357146.357150","volume":"3","author":"KR Apt","year":"1981","unstructured":"Apt, K.R.: Ten years of hoare\u2019s logic: a survey - Part I. ACM Trans. Program. Lang. Syst. 3(4), 431\u2013483 (1981). http:\/\/www.cs.cornell.edu\/Courses\/cs6860\/2010fa\/Handouts\/Apt10years.pdf","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"13_CR2","series-title":"Texts in Computer Science","volume-title":"Verification of Sequential and Concurrent Programs","author":"Krzysztof R. Apt","year":"2009","unstructured":"Apt, K.R., de Boer, F.S., Olderog, E.R.: Verification of Sequential and Concurrent Programs. Texts in Computer Science, 3rd edn., p. 502. Springer, New York (2009)"},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/978-3-319-23506-6_13","volume-title":"Correct System Design","author":"FS de Boer","year":"2015","unstructured":"de Boer, F.S., de Gouw, S.: Being and change: reasoning about invariance. In: Meyer, R., Platzer, A., Wehrheim, H. (eds.) Correct System Design. LNCS, vol. 9360, pp. 191\u2013204. Springer, Heidelberg (2015). doi:10.1007\/978-3-319-23506-6_13"},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/978-3-540-30101-1_5","volume-title":"Formal Methods for Components and Objects","author":"FS de Boer","year":"2004","unstructured":"de Boer, F.S., Pierik, C.: How to cook a complete hoare logic for your pet OO language. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2003. LNCS, vol. 3188, pp. 111\u2013133. Springer, Heidelberg (2004)"},{"issue":"1","key":"13_CR5","doi-asserted-by":"crossref","first-page":"129","DOI":"10.1145\/322108.322121","volume":"26","author":"Edmund Melson Clarke","year":"1979","unstructured":"Clarke Jr., E.M.: Programming language constructs for which it is impossible to obtain good hoare axiom systems. J. ACM 26(1), 129\u2013147 (1979). http:\/\/www.cs.cmu.edu\/~emc\/papers\/Papers%20In%20Refereed%20Journals\/79_impossible_hoareaxiom.pdf","journal-title":"Journal of the ACM"},{"issue":"1","key":"13_CR6","doi-asserted-by":"crossref","first-page":"70","DOI":"10.1137\/0207005","volume":"7","author":"Stephen A. Cook","year":"1978","unstructured":"Cook, S.A.: Soundness and completeness of an axiom system for program verification. SIAM J. Comput. 7(1), 70\u201390 (1978). http:\/\/www.cs.toronto.edu\/~sacook\/homepage\/soundness.pdf","journal-title":"SIAM Journal on Computing"},{"key":"13_CR7","unstructured":"Engelmann, B., Olderog, E.: A Sound and Complete Hoare Logic for Dynamically-Typed, Object-Oriented Programs - Extended Version. CoRR abs\/1509.08605 (2015). http:\/\/arxiv.org\/abs\/1509.08605"},{"key":"13_CR8","unstructured":"Engelmann, B., Olderog, E., Flick, N.E.: Closing the Gap - Formally Verifying Dynamically Typed Programs like Statically Typed Ones Using Hoare Logic - Extended Version. CoRR abs\/1501.02699 (2015). http:\/\/arxiv.org\/abs\/1501.02699"},{"issue":"1","key":"13_CR9","doi-asserted-by":"crossref","first-page":"31","DOI":"10.1145\/2103621.2103663","volume":"47","author":"Philippa Anne Gardner","year":"2012","unstructured":"Gardner, P., Maffeis, S., Smith, G.D.: Towards a program logic for JavaScript. In: Field, J., Hicks, M. (eds.) POPL, pp. 31\u201344. ACM (2012). http:\/\/citeseer.ist.psu.edu\/viewdoc\/summary?doi=10.1.1.221.302","journal-title":"ACM SIGPLAN Notices"},{"key":"13_CR10","unstructured":"Gorelick, G.A.: A Complete Axiomatic System for Proving Assertions about Recursive and Non-Recursive Programs. Technical report 75, Department of Computer Science, University of Toronto, Canada (1975)"},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"108","DOI":"10.1007\/3-540-09526-8_8","volume-title":"Proceedings of Mathematical Foundations of Computer Science","author":"MCB Hennessy","year":"1979","unstructured":"Hennessy, M.C.B., Plotkin, G.D.: Full abstraction for a simple programming language. Proceedings of Mathematical Foundations of Computer Science. LNCS, vol. 74, pp. 108\u2013120. Springer, New York (1979)"},{"issue":"10","key":"13_CR12","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C. A. R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12, 576\u2013580, 583 (1969). https:\/\/www.cs.cmu.edu\/~crary\/819-f09\/Hoare69.pdf","journal-title":"Communications of the ACM"},{"issue":"3","key":"13_CR13","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1016\/0304-3975(83)90009-9","volume":"24","author":"ER Olderog","year":"1983","unstructured":"Olderog, E.R.: On the notion of expressiveness and the rule of adaptation. Theoret. Comput. Sci. 24(3), 337\u2013347 (1983). http:\/\/www.sciencedirect.com\/science\/article\/pii\/0304397583900099","journal-title":"Theoret. Comput. Sci."},{"key":"13_CR14","first-page":"17","volume":"60\u201361","author":"GD Plotkin","year":"2004","unstructured":"Plotkin, G.D.: A structural approach to operational semantics. J. Logic Algebraic Program. 60\u201361, 17\u2013139 (2004).  http:\/\/homepages.inf.ed.ac.uk\/gdp\/publications\/sos_jlap.pdf","journal-title":"J. Logic Algebraic Program."},{"key":"13_CR15","doi-asserted-by":"crossref","unstructured":"Qin, S., Chawdhary, A., Xiong, W., Munro, M., Qiu, Z., Zhu, H.: Towards an Axiomatic Verification System for JavaScript. In: Proceedings of the TASE 2011, Washington, DC, pp. 133\u2013141. IEEE (2011)","DOI":"10.1109\/TASE.2011.33"}],"container-title":["Lecture Notes in Computer Science","Theory and Practice of Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-30734-3_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,12]],"date-time":"2024-07-12T12:23:10Z","timestamp":1720786990000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-30734-3_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319307336","9783319307343"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-30734-3_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"13 March 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}