An Efficient VCGen-Based Modular Verification of Relational Properties

Lionel Blatter; Nikolai Kosmatov; Virgile Prevosto; Pascale Le Gall

doi:10.1007/978-3-031-19849-6_28

An Efficient VCGen-Based Modular Verification of Relational Properties

Lionel Blatter
, Nikolai Kosmatov
, Virgile Prevosto
, Pascale Le Gall

Institute of Meteorology and Climate Research
Max Planck Institute for Security and Privacy
Université Paris-Saclay
Thales Research & Technology

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

3 Citations (Scopus)

Abstract

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.

Original language	English
Title of host publication	Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles - 11th International Symposium, ISoLA 2022, Proceedings
Editors	Tiziana Margaria, Bernhard Steffen
Publisher	Springer Science and Business Media Deutschland GmbH
Pages	498-516
Number of pages	19
ISBN (Print)	9783031198489
DOIs	https://doi.org/10.1007/978-3-031-19849-6_28
Publication status	Published - 1 Jan 2022
Externally published	Yes
Event	11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2022 - Rhodes, Greece Duration: 22 Oct 2022 → 30 Oct 2022

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	13701 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2022
Country/Territory	Greece
City	Rhodes
Period	22/10/22 → 30/10/22

Access to Document

10.1007/978-3-031-19849-6_28

Cite this

Blatter, L., Kosmatov, N., Prevosto, V., & Le Gall, P. (2022). An Efficient VCGen-Based Modular Verification of Relational Properties. In T. Margaria, & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles - 11th International Symposium, ISoLA 2022, Proceedings (pp. 498-516). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 13701 LNCS). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-031-19849-6_28

Blatter, Lionel ; Kosmatov, Nikolai ; Prevosto, Virgile et al. / An Efficient VCGen-Based Modular Verification of Relational Properties. Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles - 11th International Symposium, ISoLA 2022, Proceedings. editor / Tiziana Margaria ; Bernhard Steffen. Springer Science and Business Media Deutschland GmbH, 2022. pp. 498-516 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{2b1d778995494fca9fdab97698331413,

title = "An Efficient VCGen-Based Modular Verification of Relational Properties",

abstract = "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.",

author = "Lionel Blatter and Nikolai Kosmatov and Virgile Prevosto and \{Le Gall\}, Pascale",

note = "Publisher Copyright: {\textcopyright} 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.; 11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2022 ; Conference date: 22-10-2022 Through 30-10-2022",

year = "2022",

month = jan,

day = "1",

doi = "10.1007/978-3-031-19849-6\_28",

language = "English",

isbn = "9783031198489",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Science and Business Media Deutschland GmbH",

pages = "498--516",

editor = "Tiziana Margaria and Bernhard Steffen",

booktitle = "Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles - 11th International Symposium, ISoLA 2022, Proceedings",

}

Blatter, L, Kosmatov, N, Prevosto, V & Le Gall, P 2022, An Efficient VCGen-Based Modular Verification of Relational Properties. in T Margaria & B Steffen (eds), Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles - 11th International Symposium, ISoLA 2022, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 13701 LNCS, Springer Science and Business Media Deutschland GmbH, pp. 498-516, 11th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, ISoLA 2022, Rhodes, Greece, 22/10/22. https://doi.org/10.1007/978-3-031-19849-6_28

An Efficient VCGen-Based Modular Verification of Relational Properties. / Blatter, Lionel; Kosmatov, Nikolai; Prevosto, Virgile et al.
Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles - 11th International Symposium, ISoLA 2022, Proceedings. ed. / Tiziana Margaria; Bernhard Steffen. Springer Science and Business Media Deutschland GmbH, 2022. p. 498-516 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 13701 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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

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.

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 -

Blatter L, Kosmatov N, Prevosto V, Le Gall P. An Efficient VCGen-Based Modular Verification of Relational Properties. In Margaria T, Steffen B, editors, Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles - 11th International Symposium, ISoLA 2022, Proceedings. Springer Science and Business Media Deutschland GmbH. 2022. p. 498-516. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-031-19849-6_28

An Efficient VCGen-Based Modular Verification of Relational Properties

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this