TY - GEN
T1 - RHLE
T2 - 20th Asian Symposium on Programming Languages and Systems, APLAS 2022
AU - Dickerson, Robert
AU - Ye, Qianchuan
AU - Zhang, Michael K.
AU - Delaware, Benjamin
N1 - Publisher Copyright:
© 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.
PY - 2022
Y1 - 2022
N2 - Hoare-style program logics are a popular and effective technique for software verification. Relational program logics are an instance of this approach that enables reasoning about relationships between the execution of two or more programs. Existing relational program logics have focused on verifying that all runs of a collection of programs do not violate a specified relational behavior. Several important relational properties, including refinement and noninterference, do not fit into this category, as they also mandate the existence of specific desirable executions. This paper presents RHLE, a logic for verifying these sorts of relational ∀ ∃ properties. Key to our approach is a novel form of function specification that employs a variant of ghost variables to ensure that valid implementations exhibit certain behaviors. We have used a program verifier based on RHLE to verify a diverse set of relational ∀ ∃ properties drawn from the literature.
AB - Hoare-style program logics are a popular and effective technique for software verification. Relational program logics are an instance of this approach that enables reasoning about relationships between the execution of two or more programs. Existing relational program logics have focused on verifying that all runs of a collection of programs do not violate a specified relational behavior. Several important relational properties, including refinement and noninterference, do not fit into this category, as they also mandate the existence of specific desirable executions. This paper presents RHLE, a logic for verifying these sorts of relational ∀ ∃ properties. Key to our approach is a novel form of function specification that employs a variant of ghost variables to ensure that valid implementations exhibit certain behaviors. We have used a program verifier based on RHLE to verify a diverse set of relational ∀ ∃ properties drawn from the literature.
UR - https://www.scopus.com/pages/publications/85144478047
U2 - 10.1007/978-3-031-21037-2_4
DO - 10.1007/978-3-031-21037-2_4
M3 - Conference contribution
AN - SCOPUS:85144478047
SN - 9783031210365
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 67
EP - 87
BT - Programming Languages and Systems - 20th Asian Symposium, APLAS 2022, Proceedings
A2 - Sergey, Ilya
PB - Springer Science and Business Media Deutschland GmbH
Y2 - 5 December 2022 through 5 December 2022
ER -