TY - GEN
T1 - The WhyRel Prototype for Modular Relational Verification of Pointer Programs
AU - Nagasamudram, Ramana
AU - Banerjee, Anindya
AU - Naumann, David A.
N1 - Publisher Copyright:
© 2023, The Author(s).
PY - 2023
Y1 - 2023
N2 - Verifying relations between programs arises as a task in various verification contexts such as optimizing transformations, relating new versions of programs with older versions (regression verification), and noninterference. However, relational verification for programs acting on dynamically allocated mutable state is not well supported by existing tools, which provide a high level of automation at the cost of restricting the programs considered. Auto-active tools, on the other hand, require more user interaction but enable verification of a broader class of programs. This article presents WhyRel, a tool for the auto-active verification of relational properties of pointer programs based on relational region logic. WhyRel is evaluated through verification case studies, relying on SMT solvers orchestrated by the Why3 platform on which it builds. Case studies include establishing representation independence of ADTs, showing noninterference, and challenge problems from recent literature.
AB - Verifying relations between programs arises as a task in various verification contexts such as optimizing transformations, relating new versions of programs with older versions (regression verification), and noninterference. However, relational verification for programs acting on dynamically allocated mutable state is not well supported by existing tools, which provide a high level of automation at the cost of restricting the programs considered. Auto-active tools, on the other hand, require more user interaction but enable verification of a broader class of programs. This article presents WhyRel, a tool for the auto-active verification of relational properties of pointer programs based on relational region logic. WhyRel is evaluated through verification case studies, relying on SMT solvers orchestrated by the Why3 platform on which it builds. Case studies include establishing representation independence of ADTs, showing noninterference, and challenge problems from recent literature.
KW - auto-active verification
KW - data abstraction
KW - local reasoning
KW - relational verification
UR - http://www.scopus.com/inward/record.url?scp=85161468730&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85161468730&partnerID=8YFLogxK
U2 - 10.1007/978-3-031-30820-8_11
DO - 10.1007/978-3-031-30820-8_11
M3 - Conference contribution
AN - SCOPUS:85161468730
SN - 9783031308192
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 133
EP - 151
BT - Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Proceedings
A2 - Sankaranarayanan, Sriram
A2 - Sharygina, Natasha
T2 - 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2023, held as part of the 26th European Joint Conferences on Theory and Practice of Software, ETAPS 2023
Y2 - 22 April 2023 through 27 April 2023
ER -