Deductive Verification with Relational Properties

Modular deductive verification provides a sound and powerful technique to establish that any call to a given function respects its given specification. However, relational properties, i.e. properties relating several function calls, are not supported. This short paper presents an original automated technique for specification and verification of such properties using the classic deductive verification approach. We illustrate the proposed technique by comprehensive examples and present its implementation as a Frama-C plugin, named RPP.