TY - GEN
T1 - An Efficient VCGen-Based Modular Verification of Relational Properties
AU - Blatter, Lionel
AU - Kosmatov, Nikolai
AU - Prevosto, Virgile
AU - Le Gall, Pascale
N1 - Publisher Copyright:
© 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.
PY - 2022/1/1
Y1 - 2022/1/1
N2 - Deductive verification typically relies on function contracts that specify the behavior of each function for a single function call. Relational properties link several function calls together within a single specification. They can express more advanced properties of a given function or relate calls to different functions, possibly run in parallel. However, relational properties cannot be expressed and verified directly in the traditional setting of modular deductive verification. Recent work proposed a new technique for relational property verification that relies on a verification condition generator to produce logical formulas that must be verified to ensure a given relational property. This paper presents an overview of this approach and proposes important enhancements. We integrate an optimized verification condition generator and extend the underlying theory to show how relational properties can be proved in a modular way, where one relational property can be used to prove another one, like in modular verification of function contracts. Our results have been fully formalized and proved sound in the Coq proof assistant.
AB - Deductive verification typically relies on function contracts that specify the behavior of each function for a single function call. Relational properties link several function calls together within a single specification. They can express more advanced properties of a given function or relate calls to different functions, possibly run in parallel. However, relational properties cannot be expressed and verified directly in the traditional setting of modular deductive verification. Recent work proposed a new technique for relational property verification that relies on a verification condition generator to produce logical formulas that must be verified to ensure a given relational property. This paper presents an overview of this approach and proposes important enhancements. We integrate an optimized verification condition generator and extend the underlying theory to show how relational properties can be proved in a modular way, where one relational property can be used to prove another one, like in modular verification of function contracts. Our results have been fully formalized and proved sound in the Coq proof assistant.
UR - https://www.scopus.com/pages/publications/85142759725
U2 - 10.1007/978-3-031-19849-6_28
DO - 10.1007/978-3-031-19849-6_28
M3 - Conference contribution
AN - SCOPUS:85142759725
SN - 9783031198489
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 498
EP - 516
BT - Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles - 11th International Symposium, ISoLA 2022, Proceedings
A2 - Margaria, Tiziana
A2 - Steffen, Bernhard
PB - Springer Science and Business Media Deutschland GmbH
T2 - 11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2022
Y2 - 22 October 2022 through 30 October 2022
ER -