Static and Dynamic Verification of Relational Properties on Self-Composed C Code

Abstract : Function contracts are a well-established way of formally specifying the intended behavior of a function. However, they usually only describe what should happen during a single call. Relational properties, on the other hand, link several function calls. They include such properties as non-interference, continuity and monotonicity. Other examples relate sequences of function calls, for instance, to show that decrypting an encrypted message with the appropriate key gives back the original message. Such properties cannot be expressed directly in the traditional setting of modular deductive verification, but are amenable to verification through self-composition. This paper presents a verification technique dedicated to relational properties in C programs and its implementation in the form of a FRAMA-C plugin called RPP and based on self-composition. It supports functions with side effects and recursive functions. The proposed approach makes it possible to prove a relational property, to check it at runtime, to generate a counterexample using testing and to use it as a hypothesis in the subsequent verification. Our initial experiments on existing benchmarks confirm that the proposed technique is helpful for static and dynamic analysis of relational properties.
Document type :
Conference papers
Complete list of metadatas

Cited literature [20 references]  Display  Hide  Download

https://hal-cea.archives-ouvertes.fr/cea-01835470
Contributor : Virgile Prevosto <>
Submitted on : Wednesday, July 11, 2018 - 1:58:28 PM
Last modification on : Thursday, February 7, 2019 - 4:50:37 PM
Long-term archiving on : Saturday, October 13, 2018 - 2:10:37 AM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : cea-01835470, version 1

Collections

Citation

Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prévosto, Guillaume Petiot. Static and Dynamic Verification of Relational Properties on Self-Composed C Code. Tests and Proofs - TAP, Jun 2018, Toulouse, France. ⟨cea-01835470⟩

Share

Metrics

Record views

95

Files downloads

143