{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T02:12:14Z","timestamp":1742955134904,"version":"3.40.3"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031177149"},{"type":"electronic","value":"9783031177156"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"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":[[2022]]},"DOI":"10.1007\/978-3-031-17715-6_19","type":"book-chapter","created":{"date-parts":[[2022,10,2]],"date-time":"2022-10-02T09:02:27Z","timestamp":1664701347000},"page":"290-304","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["A Matching Logic Foundation for\u00a0Alk"],"prefix":"10.1007","author":[{"given":"Alexandru-Ioan","family":"Lungu","sequence":"first","affiliation":[]},{"given":"Dorel","family":"Lucanu","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,10,3]]},"reference":[{"key":"19_CR1","series-title":"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 - From Theory to Practice","year":"2016","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification - The KeY Book - From Theory to Practice. LNCS, vol. 10001. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6"},{"key":"19_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"406","DOI":"10.1007\/978-3-031-10363-6_27","volume-title":"Theoretical Aspects of Software Engineering","author":"L Alexandru-Ioan","year":"2022","unstructured":"Alexandru-Ioan, L., Lucanu, D.: Supporting algorithm analysis with symbolic execution in ALK. In: A\u00eft-Ameur, Y., Craciun, F. (eds.) TASE 2022. LNCS, vol. 13299, pp. 406\u2013423. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-10363-6_27"},{"key":"19_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-030-30942-8_30","volume-title":"Formal Methods \u2013 The Next 30 Years","author":"A Arusoaie","year":"2019","unstructured":"Arusoaie, A., Lucanu, D.: Unification in matching logic. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 502\u2013518. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30942-8_30"},{"key":"19_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/978-3-319-02654-1_16","volume-title":"Software Language Engineering","author":"A Arusoaie","year":"2013","unstructured":"Arusoaie, A., Lucanu, D., Rusu, V.: A generic framework for symbolic execution. In: Erwig, M., Paige, R.F., Van Wyk, E. (eds.) SLE 2013. LNCS, vol. 8225, pp. 281\u2013301. Springer, Cham (2013). https:\/\/doi.org\/10.1007\/978-3-319-02654-1_16"},{"issue":"6","key":"19_CR5","doi-asserted-by":"publisher","first-page":"709","DOI":"10.1007\/s10009-014-0314-5","volume":"17","author":"F Bobot","year":"2015","unstructured":"Bobot, F., Filli\u00e2tre, J.-C., March\u00e9, C., Paskevich, A.: Let\u2019s verify this with why3. Int. J. Softw. Tools Technol. Transf. 17(6), 709\u2013727 (2015)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"19_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1007\/978-3-030-81688-9_23","volume-title":"Computer Aided Verification","author":"X Chen","year":"2021","unstructured":"Chen, X., Lin, Z., Trinh, M.-T., Ro\u015fu, G.: Towards a trustworthy semantics-based language framework via proof generation. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 477\u2013499. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_23"},{"key":"19_CR7","unstructured":"Chen, X., Lucanu, D., Ro\u015fu, G.: Initial algebra semantics in matching logic. Technical report, University of Illinois at Urbana-Champaign, July 2020. submitted. http:\/\/hdl.handle.net\/2142\/107781"},{"key":"19_CR8","doi-asserted-by":"publisher","first-page":"100638","DOI":"10.1016\/j.jlamp.2021.100638","volume":"120","author":"X Chen","year":"2021","unstructured":"Chen, X., Lucanu, D., Ro\u015fu, G.: Matching logic explained. J. Log. Algebr. Methods Program. 120, 100638 (2021)","journal-title":"J. Log. Algebr. Methods Program."},{"key":"19_CR9","unstructured":"Chen, X., Ro\u015fu, G.: Applicative matching logic. Technical report, University of Illinois at Urbana-Champaign, July 2019. http:\/\/hdl.handle.net\/2142\/104616"},{"key":"19_CR10","doi-asserted-by":"crossref","unstructured":"Chen, X., Ro\u015fu, G.: Matching mu-logic. In: Proceedings of the 34th Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS 2019) (2019, to appear)","DOI":"10.1109\/LICS.2019.8785675"},{"key":"19_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"Engineering Trustworthy Software Systems","author":"X Chen","year":"2019","unstructured":"Chen, X., Rosu, G.: SETSS\u201919 lecture notes on K. In: Bowen, J., Liu, Z. (eds.) Engineering Trustworthy Software Systems. LNCS, Springer, Cham (2019)"},{"key":"19_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"issue":"4","key":"19_CR13","doi-asserted-by":"publisher","first-page":"636","DOI":"10.1145\/321420.321422","volume":"14","author":"RW Floyd","year":"1967","unstructured":"Floyd, R.W.: Nondeterministic algorithms. J. ACM 14(4), 636\u2013644 (1967)","journal-title":"J. ACM"},{"key":"19_CR14","series-title":"Studies in Cognitive Systems","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/978-94-011-1793-7_4","volume-title":"Program Verification","author":"RW Floyd","year":"1993","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Colburn, T.R., Fetzer, J.H., Rankin, T.L. (eds.) Program Verification. Studies in Cognitive Systems, vol. 14, pp. 65\u201381. Springer, Dordrecht (1993). https:\/\/doi.org\/10.1007\/978-94-011-1793-7_4"},{"issue":"10","key":"19_CR15","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"},{"key":"19_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/978-3-319-49812-6_7","volume-title":"Deductive Software Verification \u2013 The KeY Book","author":"M Huisman","year":"2016","unstructured":"Huisman, M., Ahrendt, W., Grahl, D., Hentschel, M.: Formal specification with the java modeling language. In: Ahrendt, W., Beckert, B., Bubel, R., Hahnle, R., Schmitt, P., Ulbrich, M. (eds.) Deductive Software Verification \u2013 The KeY Book. LNCS, vol. 10001, pp. 193\u2013241. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6_7"},{"key":"19_CR17","volume-title":"Data Flow Analysis - Theory and Practice","author":"UP Khedker","year":"2009","unstructured":"Khedker, U.P., Sanyal, A., Karkare, B.: Data Flow Analysis - Theory and Practice. CRC Press, Boca Raton (2009)"},{"key":"19_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1007\/978-3-319-46982-9_7","volume-title":"Runtime Verification","author":"N Kosmatov","year":"2016","unstructured":"Kosmatov, N., Signoles, J.: Frama-C, A collaborative framework for C code verification: tutorial synopsis. In: Falcone, Y., S\u00e1nchez, C. (eds.) RV 2016. LNCS, vol. 10012, pp. 92\u2013115. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46982-9_7"},{"key":"19_CR19","unstructured":"Leino, K.R.M.: This is boogie 2. manuscript KRML 178(131), 9 (2008)"},{"key":"19_CR20","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20"},{"key":"19_CR21","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1016\/j.jsc.2016.07.012","volume":"80","author":"D Lucanu","year":"2017","unstructured":"Lucanu, D., Rusu, V., Arusoaie, A.: A generic framework for symbolic execution: a coinductive approach. J. Symb. Comput. 80, 125\u2013163 (2017)","journal-title":"J. Symb. Comput."},{"key":"19_CR22","doi-asserted-by":"crossref","unstructured":"Alexandru-Ioan, L.: Extended z3 array. In: 23th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (FROM Workshop), SYNASC 2021. IEEE (2021, to appear)","DOI":"10.1109\/SYNASC54541.2021.00052"},{"issue":"4","key":"19_CR23","first-page":"1","volume":"13","author":"G Ro\u015fu","year":"2017","unstructured":"Ro\u015fu, G.: Matching logic. Log. Methods Comput. Sci. 13(4), 1\u201361 (2017)","journal-title":"Log. Methods Comput. Sci."},{"key":"19_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-642-17796-5_9","volume-title":"Algebraic Methodology and Software Technology","author":"G Ro\u015fu","year":"2011","unstructured":"Ro\u015fu, G., Ellison, C., Schulte, W.: Matching logic: an alternative to Hoare\/Floyd logic. In: Johnson, M., Pavlovic, D. (eds.) AMAST 2010. LNCS, vol. 6486, pp. 142\u2013162. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-17796-5_9"},{"key":"19_CR25","unstructured":"Stefanescu, A., Ciob\u00e2c\u0103, \u015e., Mereuta, R., Moore, B.M., Serbanuta, T.-F., Rosu, G.: All-path reachability logic. Log. Methods Comput. Sci. 15(2) (2019)"},{"key":"19_CR26","doi-asserted-by":"crossref","unstructured":"Vogels, F., Jacobs, B., Piessens, F.: Featherweight verifast. Log. Methods Comput. Sci. 11(3) (2015)","DOI":"10.2168\/LMCS-11(3:19)2015"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2022"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-17715-6_19","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,2]],"date-time":"2022-10-02T23:04:41Z","timestamp":1664751881000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-17715-6_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031177149","9783031177156"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-17715-6_19","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"3 October 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICTAC","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Colloquium on Theoretical Aspects of Computing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Tbilisi","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Georgia","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 September 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"29 September 2022","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":"ictac2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/viam.science.tsu.ge\/clas2022\/ictac\/index.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}