{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T12:39:43Z","timestamp":1742992783699,"version":"3.40.3"},"publisher-location":"Cham","reference-count":42,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030912642"},{"type":"electronic","value":"9783030912659"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-91265-9_4","type":"book-chapter","created":{"date-parts":[[2021,11,19]],"date-time":"2021-11-19T11:26:47Z","timestamp":1637321207000},"page":"61-80","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Reasoning About Iteration and Recursion Uniformly Based on Big-Step Semantics"],"prefix":"10.1007","author":[{"given":"Ximeng","family":"Li","sequence":"first","affiliation":[]},{"given":"Qianying","family":"Zhang","sequence":"additional","affiliation":[]},{"given":"Guohui","family":"Wang","sequence":"additional","affiliation":[]},{"given":"Zhiping","family":"Shi","sequence":"additional","affiliation":[]},{"given":"Yong","family":"Guan","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,11,18]]},"reference":[{"unstructured":"The Coq proof assistant. https:\/\/coq.inria.fr\/","key":"4_CR1"},{"unstructured":"Michelson - the language of Tezos. https:\/\/www.michelson.org\/","key":"4_CR2"},{"unstructured":"The move language. https:\/\/developers.libra-china.org\/docs\/crates\/move-language\/index.html","key":"4_CR3"},{"unstructured":"A sequential imperative programming language - syntax, semantics, Hoare logics and verification environment. https:\/\/www.isa-afp.org\/entries\/Simpl.html","key":"4_CR4"},{"unstructured":"Solidity. https:\/\/docs.soliditylang.org\/en\/v0.8.0\/","key":"4_CR5"},{"unstructured":"VCC: A verifier for concurrent C. https:\/\/www.microsoft.com\/en-us\/research\/project\/vcc-a-verifier-for-concurrent-c\/","key":"4_CR6"},{"unstructured":"Yul. https:\/\/docs.soliditylang.org\/en\/v0.8.0\/yul.html","key":"4_CR7"},{"unstructured":"Formalization of the verification technique in Coq (2021). https:\/\/github.com\/lixm\/ind-verify\/tree\/master","key":"4_CR8"},{"key":"4_CR9","series-title":"From Theory to Practice. Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-49812-6","volume-title":"Deductive Software Verification - The KeY Book","year":"2016","unstructured":"Ahrendt, W., Beckert, B., Bubel, R. (eds.): Deductive Software Verification - The KeY Book. From Theory to Practice. Lecture Notes in Computer Science, vol. 10001. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-19718-5_1","volume-title":"Programming Languages and Systems","author":"AW Appel","year":"2011","unstructured":"Appel, A.W.: Verified Software Toolchain - (invited talk). In: Barthe, G. (ed.) ESOP 2011. LNCS, vol. 6602, pp. 1\u201317. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19718-5_1"},{"issue":"3","key":"4_CR11","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/s10817-009-9148-3","volume":"43","author":"S Blazy","year":"2009","unstructured":"Blazy, S., Leroy, X.: Mechanized semantics for the Clight subset of the C language. J. Autom. Reason. 43(3), 263\u2013288 (2009)","journal-title":"J. Autom. Reason."},{"doi-asserted-by":"crossref","unstructured":"Bodin, M., Gardner, P., Jensen, T.P., Schmitt, A.: Skeletal semantics and their interpretations. Proc. ACM Program. Lang. 3(POPL), 44:1\u201344:31 (2019)","key":"4_CR12","DOI":"10.1145\/3290357"},{"doi-asserted-by":"crossref","unstructured":"Bodin, M., Jensen, T.P., Schmitt, A.: Certified abstract interpretation with pretty-big-step semantics. In: Proceedings of the 2015 Conference on Certified Programs and Proofs (CPP), pp. 29\u201340 (2015)","key":"4_CR13","DOI":"10.1145\/2676724.2693174"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-642-21437-0_20","volume-title":"FM 2011: Formal Methods","author":"A Cavalcanti","year":"2011","unstructured":"Cavalcanti, A., Wellings, A., Woodcock, J.: The safety-critical Java memory model: a formal account. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 246\u2013261. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21437-0_20"},{"doi-asserted-by":"crossref","unstructured":"Cl\u00e9ment, D., Despeyroux, J., Despeyroux, T., Kahn, G.: A simple applicative language: mini-ML. In: Proceedings of the 1986 ACM Conference on LISP and Functional Programming (LFP), pp. 13\u201327 (1986)","key":"4_CR15","DOI":"10.1145\/319838.319847"},{"doi-asserted-by":"crossref","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Fourth ACM Symposium on Principles of Programming Languages (POPL), pp. 238\u2013252 (1977)","key":"4_CR16","DOI":"10.1145\/512950.512973"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"520","DOI":"10.1007\/978-3-319-70278-0_33","volume-title":"Financial Cryptography and Data Security","author":"Y Hirai","year":"2017","unstructured":"Hirai, Y., et al.: Defining the ethereum virtual machine for interactive theorem provers. In: Brenner, M. (ed.) FC 2017. LNCS, vol. 10323, pp. 520\u2013535. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-70278-0_33"},{"issue":"10","key":"4_CR18","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(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R., He, J.: Unifying Theories of Programming. Pearson College Div (1998)","key":"4_CR19","DOI":"10.1007\/BFb0002714"},{"key":"4_CR20","doi-asserted-by":"publisher","first-page":"e20","DOI":"10.1017\/S0956796818000151","volume":"28","author":"R Jung","year":"2018","unstructured":"Jung, R., Krebbers, R., Jourdan, J., et al.: Iris from the ground up: a modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28, e20 (2018)","journal-title":"J. Funct. Program."},{"key":"4_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/BFb0039592","volume-title":"STACS 87","author":"G Kahn","year":"1987","unstructured":"Kahn, G.: Natural semantics. In: Brandenburg, F.J., Vidal-Naquet, G., Wirsing, M. (eds.) STACS 1987. LNCS, vol. 247, pp. 22\u201339. Springer, Heidelberg (1987). https:\/\/doi.org\/10.1007\/BFb0039592"},{"issue":"1","key":"4_CR22","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1007\/s11704-012-2901-5","volume":"6","author":"W Ke","year":"2012","unstructured":"Ke, W., Li, X., Liu, Z., Stolz, V.: rCOS: a formal model-driven engineering method for component-based software. Front. Comput. Sci. China 6(1), 17\u201339 (2012)","journal-title":"Front. Comput. Sci. China"},{"unstructured":"Klein, G., Nipkow, T.: Jinja is not Java. Arch. Formal Proofs (2005)","key":"4_CR23"},{"unstructured":"McCarthy, J.: Towards a mathematical science of computation. In: Proceedings of the 2nd IFIP Congress on Information Processing, pp. 21\u201328 (1962)","key":"4_CR24"},{"key":"4_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"589","DOI":"10.1007\/978-3-319-89884-1_21","volume-title":"Programming Languages and Systems","author":"B Moore","year":"2018","unstructured":"Moore, B., Pe\u00f1a, L., Rosu, G.: Program verification by coinduction. In: Ahmed, A. (ed.) ESOP 2018. LNCS, vol. 10801, pp. 589\u2013618. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89884-1_21"},{"key":"4_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/978-3-540-39724-3_27","volume-title":"Correct Hardware Design and Verification Methods","author":"JS Moore","year":"2003","unstructured":"Moore, J.S.: Inductive assertions and operational semantics. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol. 2860, pp. 289\u2013303. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-39724-3_27"},{"key":"4_CR27","series-title":"Undergraduate Topics in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84628-692-6","volume-title":"Semantics with Applications: An Appetizer","author":"HR Nielson","year":"2007","unstructured":"Nielson, H.R., Nielson, F.: Semantics with Applications: An Appetizer. Undergraduate Topics in Computer Science, Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-1-84628-692-6"},{"doi-asserted-by":"crossref","unstructured":"Nipkow, T., von Oheimb, D.: Java$${}_{light}$$ is type-safe - definitely. In: Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp. 161\u2013170 (1998)","key":"4_CR28","DOI":"10.1145\/268946.268960"},{"issue":"1\u20132","key":"4_CR29","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s00165-007-0052-5","volume":"21","author":"M Oliveira","year":"2009","unstructured":"Oliveira, M., Cavalcanti, A., Woodcock, J.: A UTP semantics for Circus. Formal Aspects Comput. 21(1\u20132), 3\u201332 (2009)","journal-title":"Formal Aspects Comput."},{"doi-asserted-by":"crossref","unstructured":"Pierce, B.C.: The science of deep specification (keynote). In: Visser, E. (ed.) Companion Proceedings of the 2016 ACM SIGPLAN International Conference on Systems, Programming, Languages and Applications: Software for Humanity (SPLASH), p. 1 (2016)","key":"4_CR30","DOI":"10.1145\/2984043.2998388"},{"unstructured":"Plotkin, G.D.: A structural approach to operational semantics. Lecture notes, DAIMI FN-19 (1981)","key":"4_CR31"},{"key":"4_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/978-3-540-45236-2_19","volume-title":"FME 2003: Formal Methods","author":"S Qin","year":"2003","unstructured":"Qin, S., Dong, J.S., Chin, W.-N.: A semantic foundation for TCOZ in unifying theories of programming. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 321\u2013340. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45236-2_19"},{"key":"4_CR33","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511626364","volume-title":"Theories of Programming Languages","author":"JC Reynolds","year":"1998","unstructured":"Reynolds, J.C.: Theories of Programming Languages. Cambridge University Press, Cambridge (1998)"},{"unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceeding of 17th IEEE Symposium on Logic in Computer Science (LICS), pp. 55\u201374 (2002)","key":"4_CR34"},{"key":"4_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-60360-3_28","volume-title":"Static Analysis","author":"DA Schmidt","year":"1995","unstructured":"Schmidt, D.A.: Natural-semantics-based abstract interpretation (preliminary version). In: Mycroft, A. (ed.) SAS 1995. LNCS, vol. 983, pp. 1\u201318. Springer, Heidelberg (1995). https:\/\/doi.org\/10.1007\/3-540-60360-3_28"},{"doi-asserted-by":"crossref","unstructured":"Sergey, I., Nagaraj, V., Johannsen, J., et al.: Safer smart contract programming with Scilla. Proc. ACM Program. Lang. 3(OOPSLA), 185:1\u2013185:30 (2019)","key":"4_CR36","DOI":"10.1145\/3360611"},{"doi-asserted-by":"crossref","unstructured":"Sewell, T.A.L., Myreen, M.O., Klein, G.: Translation validation for a verified OS kernel. In: ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pp. 471\u2013482 (2013)","key":"4_CR37","DOI":"10.1145\/2499370.2462183"},{"issue":"2\u20133","key":"4_CR38","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/s00165-020-00513-4","volume":"32","author":"F Sheng","year":"2020","unstructured":"Sheng, F., Zhu, H., He, J., et al.: Theoretical and practical approaches to the denotational semantics for MDESL based on UTP. Formal Aspects Comput. 32(2\u20133), 275\u2013314 (2020)","journal-title":"Formal Aspects Comput."},{"issue":"5","key":"4_CR39","doi-asserted-by":"publisher","first-page":"947","DOI":"10.1007\/s10817-019-09540-0","volume":"64","author":"M Sozeau","year":"2020","unstructured":"Sozeau, M., Anand, A., Boulier, S., et al.: The MetaCoq project. J. Autom. Reason. 64(5), 947\u2013999 (2020)","journal-title":"J. Autom. Reason."},{"doi-asserted-by":"crossref","unstructured":"Stefanescu, A., Park, D., Yuwen, S., et al.: Semantics-based program verifiers for all languages. In: 2016 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), pp. 74\u201391 (2016)","key":"4_CR40","DOI":"10.1145\/2983990.2984027"},{"unstructured":"Wood, G.: Ethereum: a secure decentralised generlised transaction ledger. https:\/\/gavwood.com\/paper.pdf","key":"4_CR41"},{"unstructured":"Yang, Z., Lei, H.: Lolisa: formal syntax and semantics for a subset of the Solidity programming language. CoRR, abs\/1803.09885 (2018)","key":"4_CR42"}],"container-title":["Lecture Notes in Computer Science","Dependable Software Engineering. Theories, Tools, and Applications"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-91265-9_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,12]],"date-time":"2024-09-12T17:23:11Z","timestamp":1726161791000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-91265-9_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030912642","9783030912659"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-91265-9_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"18 November 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SETTA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Dependable Software Engineering: Theories, Tools, and Applications","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Beijing","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"China","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25 November 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 November 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"setta2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/lcs.ios.ac.cn\/setta2021\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"39","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":"16","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":"41% - 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.05","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":"2.53","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)"}}]}}