Skip to Main content Skip to Navigation
Conference papers

Certified verification of relational properties

Abstract : The use of function contracts to specify the behavior of functions often remains limited to the scope of 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, such as non-interference, continuity, or monotonicity. They can also relate calls to different functions, for instance, to show that an optimized implementation is equivalent to its original counterpart. However, relational properties cannot be expressed and verified directly in the traditional setting of modular deductive verification. Self-composition has been proposed to overcome this limitation, but it requires complex transformations and additional separation hypotheses for real-life languages with pointers. We propose a novel approach that is not based on code transformation and avoids those drawbacks. It directly applies a verification condition generator to produce logical formulas that must be verified to ensure a given relational property. The approach has been fully formalized and proved sound in the Coq proof assistant.
Complete list of metadata

https://hal-cea.archives-ouvertes.fr/cea-03714381
Contributor : Contributeur MAP CEA Connect in order to contact the contributor
Submitted on : Tuesday, July 5, 2022 - 2:55:06 PM
Last modification on : Friday, July 8, 2022 - 4:15:28 AM

File

 Restricted access
To satisfy the distribution rights of the publisher, the document is embargoed until : 2022-12-17

Please log in to resquest access to the document

Identifiers

Citation

Lionel Blatter, Nikolai Kosmatov, Virgile Prevosto, Pascale Le Gall. Certified verification of relational properties. iFM 2022 : International Conference on integrated Formal Methods, Jun 2022, Lugano, Switzerland. pp.86-105, ⟨10.1007/978-3-031-07727-2_6⟩. ⟨cea-03714381⟩

Share

Metrics

Record views

13