{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,4]],"date-time":"2026-05-04T03:46:26Z","timestamp":1777866386473,"version":"3.51.4"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031982071","type":"print"},{"value":"9783031982088","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,7,9]],"date-time":"2025-07-09T00:00:00Z","timestamp":1752019200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,7,9]],"date-time":"2025-07-09T00:00:00Z","timestamp":1752019200000},"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":[[2026]]},"DOI":"10.1007\/978-3-031-98208-8_4","type":"book-chapter","created":{"date-parts":[[2025,7,13]],"date-time":"2025-07-13T17:57:05Z","timestamp":1752429425000},"page":"49-66","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["A Formal Framework for\u00a0Naturally Specifying and\u00a0Verifying Sequential Algorithms"],"prefix":"10.1007","author":[{"given":"Chengxi","family":"Yang","sequence":"first","affiliation":[]},{"given":"Shushu","family":"Wu","sequence":"additional","affiliation":[]},{"given":"Qinxiang","family":"Cao","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,7,9]]},"reference":[{"key":"4_CR1","unstructured":"Aho, A.V., Lam, M.S., Sethi, R., Ullman, J.D.: Compilers: Principles, Techniques, and Tools, 2nd edn. Addison-Wesley (2007)"},{"key":"4_CR2","unstructured":"Appel, A.W.: Verified Functional Algorithms, Software Foundations, vol.\u00a03. Electronic textbook (2024), version 1.5.5. http:\/\/softwarefoundations.cis.upenn.edu"},{"key":"4_CR3","doi-asserted-by":"publisher","first-page":"79","DOI":"10.4204\/EPTCS.400.6","volume":"400","author":"Q Cao","year":"2024","unstructured":"Cao, Q., Wu, X., Liang, Y.: A Coq library of sets for teaching denotational semantics. Electron. Proc. Theor. Comput. Sci. 400, 79\u201395 (2024). https:\/\/doi.org\/10.4204\/EPTCS.400.6","journal-title":"Electron. Proc. Theor. Comput. Sci."},{"key":"4_CR4","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 3rd edn. The MIT Press (2009)"},{"issue":"10","key":"4_CR5","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C Hoare","year":"1969","unstructured":"Hoare, C.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969). https:\/\/doi.org\/10.1145\/363235.363259","journal-title":"Commun. ACM"},{"key":"4_CR6","doi-asserted-by":"publisher","DOI":"10.1017\/S095679681800014X","volume":"28","author":"R Jung","year":"2018","unstructured":"Jung, R., Krebbers, R., Jourdan, J.H., Bizjak, A., Birkedal, L., Dreyer, D.: Iris from the ground up: a modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28, e20 (2018). https:\/\/doi.org\/10.1017\/S095679681800014X","journal-title":"J. Funct. Program."},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Knuth, D.E., Morris, J.H., Pratt, V.R.: Fast pattern matching in strings. SIAM J. Comput. 6, 323\u2013350 (1977). https:\/\/api.semanticscholar.org\/CorpusID:11697579","DOI":"10.1137\/0206024"},{"key":"4_CR8","unstructured":"Lammich, P.: Refinement for monadic programs. Archive of Formal Proofs (2012). https:\/\/isa-afp.org\/entries\/Refine_Monadic.html, Formal proof development"},{"key":"4_CR9","doi-asserted-by":"publisher","unstructured":"Lammich, P., Neumann, R.: A framework for verifying depth-first search algorithms. In: CPP 2015, pp. 137\u2013146. Association for Computing Machinery, New York (2015). https:\/\/doi.org\/10.1145\/2676724.2693165","DOI":"10.1145\/2676724.2693165"},{"issue":"1","key":"4_CR10","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1016\/0890-5401(91)90052-4","volume":"93","author":"E Moggi","year":"1991","unstructured":"Moggi, E.: Notions of computation and monads. Inf. Comput. 93(1), 55\u201392 (1991). https:\/\/doi.org\/10.1016\/0890-5401(91)90052-4","journal-title":"Inf. Comput."},{"key":"4_CR11","doi-asserted-by":"publisher","first-page":"865","DOI":"10.1017\/S0956796808006953","volume":"18","author":"A Nanevski","year":"2008","unstructured":"Nanevski, A., Morrisett, J., Birkedal, L.: Hoare type theory, polymorphism and separation. J. Funct. Program. 18, 865\u2013911 (2008). https:\/\/doi.org\/10.1017\/S0956796808006953","journal-title":"J. Funct. Program."},{"key":"4_CR12","doi-asserted-by":"publisher","unstructured":"Nigron, P., Dagand, P.E.: Reaching for the star: tale of a monad in Coq. In: Cohen, L., Kaliszyk, C. (eds.) 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), vol.\u00a0193, pp. 29:1\u201329:19. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Dagstuhl, Germany (2021). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2021.29","DOI":"10.4230\/LIPIcs.ITP.2021.29"},{"key":"4_CR13","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer, Heidelberg (2002)"},{"key":"4_CR14","unstructured":"Paulson, L.C.: Knuth\u2013Morris\u2013Pratt string search. Archive of Formal Proofs (2023). https:\/\/isa-afp.org\/entries\/KnuthMorrisPratt.html, Formal proof development"},{"key":"4_CR15","unstructured":"Pierce, B.C., et al.: Programming Language Foundations, Software Foundations, vol.\u00a02. Electronic Textbook (2024)"},{"key":"4_CR16","doi-asserted-by":"publisher","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science (LICS 2002), pp. 59\u201378. IEEE Computer Society (2002). https:\/\/doi.org\/10.1109\/LICS.2002.1029817","DOI":"10.1109\/LICS.2002.1029817"},{"key":"4_CR17","unstructured":"The Coq Development Team: The Coq reference manual \u2013 release 8.19.0 (2024). https:\/\/coq.inria.fr\/doc\/V8.19.0\/refman"},{"key":"4_CR18","doi-asserted-by":"publisher","unstructured":"Wang, S., Cao, Q., Mohan, A., Hobor, A.: Certifying graph-manipulating C programs via localizations within data structures. Proc. ACM Program. Lang. 3(OOPSLA) (2019). https:\/\/doi.org\/10.1145\/3360597","DOI":"10.1145\/3360597"},{"key":"4_CR19","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/3054.001.0001","volume-title":"The Formal Semantics of Programming Languages: An Introduction","author":"G Winskel","year":"1993","unstructured":"Winskel, G.: The Formal Semantics of Programming Languages: An Introduction. MIT Press, Cambridge (1993)"},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"Wu, S., Wu, X., Cao, Q.: Encode the $$\\forall \\exists $$ relational Hoare logic into standard Hoare logic (2025). https:\/\/arxiv.org\/abs\/2504.17444","DOI":"10.1145\/3763138"},{"key":"4_CR21","doi-asserted-by":"crossref","unstructured":"Yang, C., Wu, S., Cao, Q.: A formal framework for naturally specifying and verifying sequential algorithms (2025). https:\/\/arxiv.org\/abs\/2504.19852","DOI":"10.1007\/978-3-031-98208-8_4"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-98208-8_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,4,30]],"date-time":"2026-04-30T08:36:04Z","timestamp":1777538164000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-98208-8_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,7,9]]},"ISBN":["9783031982071","9783031982088"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-98208-8_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,7,9]]},"assertion":[{"value":"9 July 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"TASE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Theoretical Aspects of Software Engineering","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Limassol","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Cyprus","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 July 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 July 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tase2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/cyprusconferences.org\/tase2025\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}