TY - GEN
T1 - Relational Denotational and Algebraic Semantics Based on UTP
AU - Hou, Zhiru
AU - Zhu, Huibiao
N1 - Publisher Copyright:
© The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd. 2025.
PY - 2025
Y1 - 2025
N2 - Relational Hoare logic [18] extends the applicability of modular deductive verification to encompass the verification of crucial 2-run properties, such as confidentiality. Most of the current research on relational Hoare logic primarily focuses on its practical applications. However, incorporating parallel programs into the logic may further complicate the system design, which is an aspect that most research has overlooked. Therefore, this paper updates the previous system, referred to as the relational system, by incorporating parallel composition. Based on the Unifying Theories of Programming (UTP), we further explore the denotational semantics and algebraic semantics of the system with 2-runs, employing relational denotational and algebraic semantics for representation. And the study of the conditional construct and parallel composition are the crucial points. To facilitate the algebraic exploration of parallel expansion laws, we extend the system with a new concept called guarded choice, enabling the transformation of any program into a guarded choice form.
AB - Relational Hoare logic [18] extends the applicability of modular deductive verification to encompass the verification of crucial 2-run properties, such as confidentiality. Most of the current research on relational Hoare logic primarily focuses on its practical applications. However, incorporating parallel programs into the logic may further complicate the system design, which is an aspect that most research has overlooked. Therefore, this paper updates the previous system, referred to as the relational system, by incorporating parallel composition. Based on the Unifying Theories of Programming (UTP), we further explore the denotational semantics and algebraic semantics of the system with 2-runs, employing relational denotational and algebraic semantics for representation. And the study of the conditional construct and parallel composition are the crucial points. To facilitate the algebraic exploration of parallel expansion laws, we extend the system with a new concept called guarded choice, enabling the transformation of any program into a guarded choice form.
KW - Algebraic Semantics
KW - Denotational Semantics
KW - Relational Hoare Logic
KW - Unifying Theories of Programming (UTP)
UR - https://www.scopus.com/pages/publications/86000440318
U2 - 10.1007/978-981-96-1621-3_15
DO - 10.1007/978-981-96-1621-3_15
M3 - 会议稿件
AN - SCOPUS:86000440318
SN - 9789819616206
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 226
EP - 244
BT - Software Fault Prevention, Verification, and Validation - 1st International Symposium, SFPVV 2024, Proceedings
A2 - Liu, Shaoying
PB - Springer Science and Business Media Deutschland GmbH
T2 - 1st International Symposium on Software Fault Prevention, Verification, and Validation, SFPVV 2024
Y2 - 2 December 2024 through 3 December 2024
ER -