@inproceedings{b089305cc3d34b82b29aff8802db521e,
title = "RPP: Automatic proof of relational properties by self-composition",
abstract = "Self-composition provides a powerful theoretical approach to prove relational properties, i.e. properties relating several program executions, that has been applied to compare two runs of one or similar programs (in secure dataflow properties, code transformations, etc.). This tool demo paper presents RPP, an original implementation of self-composition for specification and verification of relational properties in C programs in the Frama-C platform. We consider a very general notion of relational properties invoking any finite number of function calls of possibly dissimilar functions with possible nested calls. The new tool allows the user to specify a relational property, to prove it in a completely automatic way using classic deductive verification, and to use it as a hypothesis in the proof of other properties that may rely on it.",
author = "Lionel Blatter and Nikolai Kosmatov and \{Le Gall\}, Pascale and Virgile Prevosto",
note = "Publisher Copyright: {\textcopyright} Springer-Verlag GmbH Germany 2017.; 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2017 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017 ; Conference date: 22-04-2017 Through 29-04-2017",
year = "2017",
month = jan,
day = "1",
doi = "10.1007/978-3-662-54577-5\_22",
language = "English",
isbn = "9783662545768",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "391--397",
editor = "\{Margaria \}, Tiziana and Axel Legay",
booktitle = "Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Proceedings",
}