{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,14]],"date-time":"2025-06-14T05:10:09Z","timestamp":1749877809023,"version":"3.41.0"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319519623"},{"type":"electronic","value":"9783319519630"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-51963-0_10","type":"book-chapter","created":{"date-parts":[[2017,1,10]],"date-time":"2017-01-10T06:17:39Z","timestamp":1484029059000},"page":"119-131","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Completeness of Hoare Logic Relative to the Standard Model"],"prefix":"10.1007","author":[{"given":"Zhaowei","family":"Xu","sequence":"first","affiliation":[]},{"given":"Wenhui","family":"Zhang","sequence":"additional","affiliation":[]},{"given":"Yuefei","family":"Sui","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,1,11]]},"reference":[{"key":"10_CR1","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12, 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"10_CR2","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1137\/0207005","volume":"7","author":"SA Cook","year":"1978","unstructured":"Cook, S.A.: Soundness and completeness of an axiom system for program verification. SIAM J. Comput. 7, 70\u201390 (1978)","journal-title":"SIAM J. Comput."},{"key":"10_CR3","volume-title":"Algorithmic Logic","author":"G Mirkowska","year":"1987","unstructured":"Mirkowska, G., Salwicki, A.: Algorithmic Logic. Springer, Dordrecht (1987)"},{"key":"10_CR4","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic Logic","author":"D Harel","year":"2000","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)"},{"doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS, pp. 55\u201374 (2002)","key":"10_CR5","DOI":"10.1109\/LICS.2002.1029817"},{"issue":"4","key":"10_CR6","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)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"10_CR7","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1016\/0304-3975(83)90066-X","volume":"28","author":"KR Apt","year":"1984","unstructured":"Apt, K.R.: Ten years of Hoare\u2019s logic: a survey - Part II: nondeterminism. Theoret. Comput. Sci. 28, 83\u2013109 (1984)","journal-title":"Theoret. Comput. Sci."},{"key":"10_CR8","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1007\/s001650050057","volume":"11","author":"T Kleymann","year":"1999","unstructured":"Kleymann, T.: Hoare logic and auxiliary variables. Formal Aspects Comput. 11, 541\u2013566 (1999)","journal-title":"Formal Aspects Comput."},{"doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Hoare logics in Isabelle, HOL. In: Proof and System-Reliability, pp. 341\u2013367, Kluwer Academic Publishers (2002)","key":"10_CR9","DOI":"10.1007\/978-94-010-0413-8_11"},{"key":"10_CR10","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198532132.001.0001","volume-title":"Models of Peano Arithmetic","author":"R Kaye","year":"1991","unstructured":"Kaye, R.: Models of Peano Arithmetic. Oxford University Press, New York (1991)"},{"key":"10_CR11","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1016\/0304-3975(83)90107-X","volume":"22","author":"JA Bergstra","year":"1983","unstructured":"Bergstra, J.A., Tucker, J.V.: Hoare\u2019s logic and Peano\u2019s arithmetic. Theoret. Comput. Sci. 22, 265\u2013284 (1983)","journal-title":"Theoret. Comput. Sci."},{"key":"10_CR12","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511804076","volume-title":"Computability and Logic","author":"GS Boolos","year":"2007","unstructured":"Boolos, G.S., Burgess, J.P., Jeffrey, R.C.: Computability and Logic, 5th edn. Cambridge University Press, Cambridge (2007)","edition":"5"},{"key":"10_CR13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-02460-7","volume-title":"Recursively Enumerable Sets and Degrees","author":"RI Soare","year":"1987","unstructured":"Soare, R.I.: Recursively Enumerable Sets and Degrees. Springer, Heidelberg (1987)"},{"key":"10_CR14","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(79)90058-6","volume":"8","author":"K Apt","year":"1979","unstructured":"Apt, K., Bergstra, J.A., Meertens, L.G.L.T.: Recursive assertions are not enough-or are they? Theoret. Comput. Sci. 8, 73\u201387 (1979)","journal-title":"Theoret. Comput. Sci."},{"key":"10_CR15","doi-asserted-by":"publisher","first-page":"129","DOI":"10.1145\/322108.322121","volume":"26","author":"EM Clarke","year":"1979","unstructured":"Clarke, E.M.: Programming language constructs for which it is impossible to obtain good Hoare axiom systems. J. ACM 26, 129\u2013147 (1979)","journal-title":"J. ACM"},{"doi-asserted-by":"crossref","unstructured":"Lipton, R.J.: A necessary and sufficient condition for the existence of Hoare logics. In: IEEE Symposium on Foundations of Computer Science, pp. 1\u20136 (1977)","key":"10_CR16","DOI":"10.1109\/SFCS.1977.1"},{"key":"10_CR17","doi-asserted-by":"publisher","first-page":"612","DOI":"10.1145\/2402.322394","volume":"30","author":"EM Clarke","year":"1983","unstructured":"Clarke, E.M., German, S.M., Halpern, J.Y.: Effective axiomatizations of Hoare logics. J. ACM 30, 612\u2013636 (1983)","journal-title":"J. ACM"},{"key":"10_CR18","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1016\/S0019-9958(85)80010-3","volume":"66","author":"M Grabowski","year":"1985","unstructured":"Grabowski, M.: On relative completeness of Hoare logics. Inf. Control 66, 29\u201344 (1985)","journal-title":"Inf. Control"},{"key":"10_CR19","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/0022-0000(82)90013-7","volume":"25","author":"JA Bergstra","year":"1982","unstructured":"Bergstra, J.A., Tucker, J.V.: Expressiveness and the completeness of Hoare\u2019s logic. J. Comput. Syst. Sci. 25, 267\u2013284 (1982)","journal-title":"J. Comput. Syst. Sci."},{"key":"10_CR20","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1016\/j.tcs.2015.08.004","volume":"612","author":"Z Xu","year":"2016","unstructured":"Xu, Z., Sui, Y., Zhang, W.: Completeness of Hoare logic with inputs over the standard model. Theoret. Comput. Sci. 612, 23\u201328 (2016)","journal-title":"Theoret. Comput. Sci."},{"key":"10_CR21","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1016\/S0020-0255(01)00164-5","volume":"139","author":"D Kozen","year":"2001","unstructured":"Kozen, D., Tiuryn, J.: On the completeness of propositional Hoare logic. Inf. Sci. 139, 187\u2013195 (2001)","journal-title":"Inf. Sci."},{"key":"10_CR22","volume-title":"Computability & Unsovability","author":"M Davis","year":"1982","unstructured":"Davis, M.: Computability & Unsovability. Courier Dover Publications, New York (1982)"}],"container-title":["Lecture Notes in Computer Science","SOFSEM 2017: Theory and Practice of Computer Science"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-51963-0_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,14]],"date-time":"2025-06-14T04:55:53Z","timestamp":1749876953000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-51963-0_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319519623","9783319519630"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-51963-0_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]},"assertion":[{"value":"11 January 2017","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SOFSEM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Current Trends in Theory and Practice of Informatics","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Limerick","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Ireland","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2017","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 January 2017","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 January 2017","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"43","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sofsem2017","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}