Multi-perspective Correctness of Programs

Eduard Kamburjan; Dilian Gurov

doi:10.1007/978-3-032-11176-0_6

Multi-perspective Correctness of Programs

Eduard Kamburjan
, Dilian Gurov

KTH Royal Institute of Technology

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-review

Abstract

Traditionally, programs are formally specified and verified with respect to their computational domain, disregarding the domain in which they are to be applied. This, however, is inadequate for programs that simulate processes in a specific application domain, or programs that generate data that must conform to external, domain-specific specifications. Such programs need also to be correct with respect to their application domain. This work presents a Hoare Logic that manages two different perspectives on a program during a correctness proof: the computational view and the domain view. This enables us to specify the correctness of a program in terms of the domain without referring to the computational details, but at the same time to interpret failed proof attempts in the domain. For domain specification, we illustrate the use of description logics and base our approach on semantic lifting, an approach to interpret a program as a knowledge graph. We present a calculus that uses translations between both kinds of assertions, thus separating the concerns in specification, but enabling the use of description logic in verification.

Original language	English
Title of host publication	Theoretical Aspects of Computing -- ICTAC 2025
Editors	Zhiming Liu, Adnane Saoud, Heike Wehrheim
Number of pages	18
Volume	16237
Place of Publication	Cham
Publisher	Springer Nature Switzerland
Publication date	23 Nov 2025
Pages	69-86
ISBN (Print)	978-3-032-11176-0
ISBN (Electronic)	978-3-032-11176-0
DOIs	https://doi.org/10.1007/978-3-032-11176-0_6
Publication status	Published - 23 Nov 2025
Event	International Colloquium on Theoretical Aspects of Computing - Marrakech, Morocco Duration: 24 Nov 2025 → 28 Nov 2025 Conference number: 22 https://ictac.isp.uni-luebeck.de/

Conference

Conference	International Colloquium on Theoretical Aspects of Computing
Number	22
Country/Territory	Morocco
City	Marrakech
Period	24/11/2025 → 28/11/2025
Internet address	https://ictac.isp.uni-luebeck.de/

Series	Lecture Notes in Computer Science
Volume	16237

Keywords

Hoare logic
domain-specific specification
Description Logics
semantic lifting
knowledge graph

Access to Document

10.1007/978-3-032-11176-0_6Licence: Unspecified

Cite this

@inproceedings{8611d8d8fcb64e80ad3ffdf27e6bdc68,

title = "Multi-perspective Correctness of Programs",

abstract = "Traditionally, programs are formally specified and verified with respect to their computational domain, disregarding the domain in which they are to be applied. This, however, is inadequate for programs that simulate processes in a specific application domain, or programs that generate data that must conform to external, domain-specific specifications. Such programs need also to be correct with respect to their application domain. This work presents a Hoare Logic that manages two different perspectives on a program during a correctness proof: the computational view and the domain view. This enables us to specify the correctness of a program in terms of the domain without referring to the computational details, but at the same time to interpret failed proof attempts in the domain. For domain specification, we illustrate the use of description logics and base our approach on semantic lifting, an approach to interpret a program as a knowledge graph. We present a calculus that uses translations between both kinds of assertions, thus separating the concerns in specification, but enabling the use of description logic in verification.",

keywords = "Hoare logic, domain-specific specification, Description Logics, semantic lifting, knowledge graph",

author = "Eduard Kamburjan and Dilian Gurov",

year = "2025",

month = nov,

day = "23",

doi = "10.1007/978-3-032-11176-0\_6",

language = "English",

isbn = "978-3-032-11176-0",

volume = "16237",

series = "Lecture Notes in Computer Science",

pages = "69--86",

editor = "Zhiming Liu and Adnane Saoud and Heike Wehrheim",

booktitle = "Theoretical Aspects of Computing -- ICTAC 2025",

publisher = "Springer Nature Switzerland",

note = "International Colloquium on Theoretical Aspects of Computing, ICTAC 2025 ; Conference date: 24-11-2025 Through 28-11-2025",

url = "https://ictac.isp.uni-luebeck.de/",

}

Kamburjan, E & Gurov, D 2025, Multi-perspective Correctness of Programs. in Z Liu, A Saoud & H Wehrheim (eds), Theoretical Aspects of Computing -- ICTAC 2025. vol. 16237, Springer Nature Switzerland, Cham, Lecture Notes in Computer Science, vol. 16237, pp. 69-86, International Colloquium on Theoretical Aspects of Computing, Marrakech, Morocco, 24/11/2025. https://doi.org/10.1007/978-3-032-11176-0_6

Multi-perspective Correctness of Programs. / Kamburjan, Eduard; Gurov, Dilian.
Theoretical Aspects of Computing -- ICTAC 2025. ed. / Zhiming Liu; Adnane Saoud; Heike Wehrheim. Vol. 16237 Cham: Springer Nature Switzerland, 2025. p. 69-86 (Lecture Notes in Computer Science, Vol. 16237).

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-review

TY - GEN

T1 - Multi-perspective Correctness of Programs

AU - Kamburjan, Eduard

AU - Gurov, Dilian

N1 - Conference code: 22

PY - 2025/11/23

Y1 - 2025/11/23

N2 - Traditionally, programs are formally specified and verified with respect to their computational domain, disregarding the domain in which they are to be applied. This, however, is inadequate for programs that simulate processes in a specific application domain, or programs that generate data that must conform to external, domain-specific specifications. Such programs need also to be correct with respect to their application domain. This work presents a Hoare Logic that manages two different perspectives on a program during a correctness proof: the computational view and the domain view. This enables us to specify the correctness of a program in terms of the domain without referring to the computational details, but at the same time to interpret failed proof attempts in the domain. For domain specification, we illustrate the use of description logics and base our approach on semantic lifting, an approach to interpret a program as a knowledge graph. We present a calculus that uses translations between both kinds of assertions, thus separating the concerns in specification, but enabling the use of description logic in verification.

AB - Traditionally, programs are formally specified and verified with respect to their computational domain, disregarding the domain in which they are to be applied. This, however, is inadequate for programs that simulate processes in a specific application domain, or programs that generate data that must conform to external, domain-specific specifications. Such programs need also to be correct with respect to their application domain. This work presents a Hoare Logic that manages two different perspectives on a program during a correctness proof: the computational view and the domain view. This enables us to specify the correctness of a program in terms of the domain without referring to the computational details, but at the same time to interpret failed proof attempts in the domain. For domain specification, we illustrate the use of description logics and base our approach on semantic lifting, an approach to interpret a program as a knowledge graph. We present a calculus that uses translations between both kinds of assertions, thus separating the concerns in specification, but enabling the use of description logic in verification.

KW - Hoare logic

KW - domain-specific specification

KW - Description Logics

KW - semantic lifting

KW - knowledge graph

U2 - 10.1007/978-3-032-11176-0_6

DO - 10.1007/978-3-032-11176-0_6

M3 - Article in proceedings

SN - 978-3-032-11176-0

VL - 16237

T3 - Lecture Notes in Computer Science

SP - 69

EP - 86

BT - Theoretical Aspects of Computing -- ICTAC 2025

A2 - Liu, Zhiming

A2 - Saoud, Adnane

A2 - Wehrheim, Heike

PB - Springer Nature Switzerland

CY - Cham

T2 - International Colloquium on Theoretical Aspects of Computing

Y2 - 24 November 2025 through 28 November 2025