{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:13:29Z","timestamp":1775790809032,"version":"3.50.1"},"publisher-location":"Cham","reference-count":33,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783032111753","type":"print"},{"value":"9783032111760","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,11,23]],"date-time":"2025-11-23T00:00:00Z","timestamp":1763856000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,11,23]],"date-time":"2025-11-23T00:00:00Z","timestamp":1763856000000},"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-032-11176-0_6","type":"book-chapter","created":{"date-parts":[[2025,11,22]],"date-time":"2025-11-22T20:11:19Z","timestamp":1763842279000},"page":"69-86","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Multi-perspective Correctness of\u00a0Programs"],"prefix":"10.1007","author":[{"given":"Eduard","family":"Kamburjan","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dilian","family":"Gurov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,11,23]]},"reference":[{"key":"6_CR1","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1007\/978-3-642-40885-4_12","volume-title":"Frontiers of Combining Systems","author":"F Baader","year":"2013","unstructured":"Baader, F., Zarrie\u00df, B.: Verification of golog programs over description logic actions. In: Fontaine, P., Ringeissen, C., Schmidt, R.A. (eds.) FroCoS 2013. LNCS (LNAI), vol. 8152, pp. 181\u2013196. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40885-4_12"},{"key":"6_CR2","doi-asserted-by":"crossref","unstructured":"Baumann, C., Beckert, B., Blasum, H., Bormer, T.: Lessons learned from microkernel verification \u2013 specification is the new bottleneck. In: SSV. EPTCS, vol.\u00a0102, pp. 18\u201332 (2012)","DOI":"10.4204\/EPTCS.102.4"},{"key":"6_CR3","unstructured":"B\u00f6rger, E., St\u00e4rk, R.F.: Abstract State Machines. A Method for High-Level System Design and Analysis. Springer, Heidelberg (2003). http:\/\/www.springer.com\/computer\/swe\/book\/978-3-540-00702-9"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1007\/978-3-319-11558-0_36","volume-title":"Logics in Artificial Intelligence","author":"D Calvanese","year":"2014","unstructured":"Calvanese, D., Ceylan, \u0130\u0130, Montali, M., Santoso, A.: Verification of context-sensitive knowledge and action bases. In: Ferm\u00e9, E., Leite, J. (eds.) JELIA 2014. LNCS (LNAI), vol. 8761, pp. 514\u2013528. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-11558-0_36"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Calvanese, D., Gianola, A., Mazzullo, A., Montali, M.: SMT safety verification of ontology-based processes. In: AAAI, pp. 6271\u20136279. AAAI Press (2023)","DOI":"10.1609\/aaai.v37i5.25772"},{"key":"6_CR6","doi-asserted-by":"publisher","unstructured":"Cook, S.A.: Soundness and completeness of an axiom system for program verification. SIAM J. Comput. 7(1), 70\u201390 (1978). https:\/\/doi.org\/10.1137\/0207005","DOI":"10.1137\/0207005"},{"key":"6_CR7","unstructured":"Deng, X., Haarslev, V., Shiri, N.: A framework for explaining reasoning in description logics. In: ExaCt. AAAI Technical Report, vol. FS-05-04, pp. 55\u201361. AAAI Press (2005)"},{"issue":"6","key":"6_CR8","doi-asserted-by":"publisher","first-page":"885","DOI":"10.1007\/s00165-021-00549-0","volume":"33","author":"C Dubslaff","year":"2021","unstructured":"Dubslaff, C., Koopmann, P., Turhan, A.: Enhancing probabilistic model checking with ontologies. Formal Aspects Comput. 33(6), 885\u2013921 (2021)","journal-title":"Formal Aspects Comput."},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"Fagin, R., Halpern, J.Y., Moses, Y., Vardi, M.Y.: Reasoning About Knowledge. MIT Press, Cambridge (1995)","DOI":"10.7551\/mitpress\/5803.001.0001"},{"issue":"1\u20132","key":"6_CR10","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1016\/S0004-3702(00)00031-X","volume":"121","author":"GD Giacomo","year":"2000","unstructured":"Giacomo, G.D., Lesp\u00e9rance, Y., Levesque, H.J.: ConGolog, a concurrent programming language based on the situation calculus. Artif. Intell. 121(1\u20132), 109\u2013169 (2000)","journal-title":"Artif. Intell."},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/978-3-030-64354-6_11","volume-title":"Deductive Software Verification: Future Perspectives","author":"S Grebing","year":"2020","unstructured":"Grebing, S., Ulbrich, M.: Usability recommendations for user guidance in deductive program verification. In: Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Ulbrich, M. (eds.) Deductive Software Verification: Future Perspectives. LNCS, vol. 12345, pp. 261\u2013284. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-64354-6_11"},{"key":"6_CR12","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/978-3-319-98047-8_8","volume-title":"Principled Software Development","author":"D Gurov","year":"2018","unstructured":"Gurov, D., Westman, J.: A hoare logic contract theory: an exercise in denotational semantics. In: Principled Software Development, pp. 119\u2013127. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-98047-8_8"},{"key":"6_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/978-3-319-91908-9_18","volume-title":"Computing and Software Science","author":"R H\u00e4hnle","year":"2019","unstructured":"H\u00e4hnle, R., Huisman, M.: Deductive software verification: from pen-and-paper proofs to industrial tools. In: Steffen, B., Woeginger, G. (eds.) Computing and Software Science. LNCS, vol. 10000, pp. 345\u2013373. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-319-91908-9_18"},{"key":"6_CR14","doi-asserted-by":"publisher","first-page":"651","DOI":"10.1613\/jair.3826","volume":"46","author":"BB Hariri","year":"2013","unstructured":"Hariri, B.B., Calvanese, D., Montali, M., Giacomo, G.D., Masellis, R.D., Felli, P.: Description logic knowledge and action bases. J. Artif. Intell. Res. 46, 651\u2013686 (2013)","journal-title":"J. Artif. Intell. Res."},{"key":"6_CR15","doi-asserted-by":"publisher","unstructured":"Haubner, A.W.: Inspecting Java Program States with Semantic Web Technologies. Master\u2019s thesis, Technische Universit\u00e4t Darmstadt, Darmstadt (2022). https:\/\/doi.org\/10.26083\/tuprints-00022143, the software developed as part of this thesis is available on GitHub. The Semantic Java Debugger: https:\/\/github.com\/ahbnr\/SemanticJavaDebugger The jdi2owl library: https:\/\/github.com\/ahbnr\/jdi2owl","DOI":"10.26083\/tuprints-00022143"},{"key":"6_CR16","unstructured":"Horrocks, I., Sattler, U.: Ontology reasoning in the SHOQ(D) description logic. In: IJCAI, pp. 199\u2013204. Morgan Kaufmann (2001)"},{"key":"6_CR17","unstructured":"Kamburjan, E., Gurov, D.: A Hoare logic for domain specification (full version) (2024). https:\/\/arxiv.org\/abs\/2402.00452"},{"key":"6_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/978-3-030-77385-4_8","volume-title":"The Semantic Web","author":"E Kamburjan","year":"2021","unstructured":"Kamburjan, E., Klungre, V.N., Schlatte, R., Johnsen, E.B., Giese, M.: Programming and debugging with semantically lifted states. In: Verborgh, R., et al. (eds.) ESWC 2021. LNCS, vol. 12731, pp. 126\u2013142. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-77385-4_8"},{"key":"6_CR19","unstructured":"Kamburjan, E., Kostylev, E.V.: Type checking semantically lifted programs via query containment under entailment regimes. In: Description Logics. CEUR Workshop Proceedings, vol.\u00a02954. CEUR-WS.org (2021)"},{"key":"6_CR20","doi-asserted-by":"publisher","unstructured":"Knapp, A., M\u00fchlberger, H., Reus, B.: Interpreting knowledge-based programs. In: ESOP. Lecture Notes in Computer Science, vol. 13990, pp. 253\u2013280. Springer, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-30044-8_10","DOI":"10.1007\/978-3-031-30044-8_10"},{"key":"6_CR21","doi-asserted-by":"crossref","unstructured":"Koopmann, P., Del-Pinto, W., Tourret, S., Schmidt, R.A.: Signature-based abduction for expressive description logics. In: KR, pp. 592\u2013602 (2020)","DOI":"10.24963\/kr.2020\/59"},{"key":"6_CR22","doi-asserted-by":"crossref","unstructured":"Krisnadhi, A., Hitzler, P.: The stub metapattern. In: WOP@ISWC. Studies on the Semantic Web, vol.\u00a032, pp. 39\u201345. IOS Press (2016)","DOI":"10.3233\/978-1-61499-826-6-39"},{"key":"6_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"750","DOI":"10.1007\/978-3-662-54434-1_28","volume-title":"Programming Languages and Systems","author":"M Leinberger","year":"2017","unstructured":"Leinberger, M., L\u00e4mmel, R., Staab, S.: The essence of functional programming on semantic data. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 750\u2013776. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54434-1_28"},{"key":"6_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"366","DOI":"10.1007\/978-3-030-62419-4_21","volume-title":"The Semantic Web \u2013 ISWC 2020","author":"M Leinberger","year":"2020","unstructured":"Leinberger, M., Seifer, P., Rienstra, T., L\u00e4mmel, R., Staab, S.: Deciding SHACL shape containment through description logics reasoning. In: Pan, J.Z., et al. (eds.) ISWC 2020. LNCS, vol. 12506, pp. 366\u2013383. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-62419-4_21"},{"key":"6_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/978-3-030-30793-6_23","volume-title":"The Semantic Web \u2013 ISWC 2019","author":"M Leinberger","year":"2019","unstructured":"Leinberger, M., Seifer, P., Schon, C., L\u00e4mmel, R., Staab, S.: Type checking program code using SHACL. In: Ghidini, C., et al. (eds.) ISWC 2019. LNCS, vol. 11778, pp. 399\u2013417. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-30793-6_23"},{"issue":"1\u20133","key":"6_CR26","doi-asserted-by":"publisher","first-page":"59","DOI":"10.1016\/S0743-1066(96)00121-5","volume":"31","author":"HJ Levesque","year":"1997","unstructured":"Levesque, H.J., Reiter, R., Lesp\u00e9rance, Y., Lin, F., Scherl, R.B.: GOLOG: a logic programming language for dynamic domains. J. Log. Program. 31(1\u20133), 59\u201383 (1997)","journal-title":"J. Log. Program."},{"issue":"1","key":"6_CR27","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1093\/jigpal\/1.1.99","volume":"1","author":"MC Mayer","year":"1993","unstructured":"Mayer, M.C., Pirri, F.: First order abduction via tableau and sequent calculi. Log. J. IGPL 1(1), 99\u2013117 (1993)","journal-title":"Log. J. IGPL"},{"key":"6_CR28","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. Springer, Heidelberg (2007)"},{"key":"6_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"8","DOI":"10.1007\/978-3-319-48869-1_2","volume-title":"Verified Software. Theories, Tools, and Experiments","author":"KY Rozier","year":"2016","unstructured":"Rozier, K.Y.: Specification: the biggest bottleneck in formal methods and autonomy. In: Blazy, S., Chechik, M. (eds.) VSTTE 2016. LNCS, vol. 9971, pp. 8\u201326. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-48869-1_2"},{"key":"6_CR30","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/978-3-540-30227-8_35","volume-title":"Logics in Artificial Intelligence","author":"S Schlobach","year":"2004","unstructured":"Schlobach, S.: Explaining subsumption by optimal interpolation. In: Alferes, J.J., Leite, J. (eds.) JELIA 2004. LNCS (LNAI), vol. 3229, pp. 413\u2013425. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30227-8_35"},{"key":"6_CR31","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":"6_CR32","unstructured":"Zarrie\u00df, B.: Verification of golog programs over description logic actions. Ph.D. thesis, Dresden University of Technology, Germany (2018)"},{"key":"6_CR33","doi-asserted-by":"crossref","unstructured":"Zarrie\u00df, B., Cla\u00dfen, J.: Verification of knowledge-based programs over description logic actions. In: IJCAI. AAAI Press (2015)","DOI":"10.25368\/2022.216"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing \u2013 ICTAC 2025"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-032-11176-0_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T11:09:52Z","timestamp":1770721792000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-032-11176-0_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,11,23]]},"ISBN":["9783032111753","9783032111760"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-032-11176-0_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,11,23]]},"assertion":[{"value":"23 November 2025","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":"Marrakesh","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Morocco","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":"24 November 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28 November 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ictac2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ictac2025.digital-hub.sh\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}