Top

Published in:

2017 | OriginalPaper | Chapter

RPP: Automatic Proof of Relational Properties by Self-composition

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

Published in: Tools and Algorithms for the Construction and Analysis of Systems

Publisher: Springer Berlin Heidelberg

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter HQSpre – An Effective Preprocessor for QBF and DQBF

next chapter autoCode4: Structural Controller Synthesis

http://www.systematic-paris-region.org/en/projets/pisco.

Technically, a special “valid under condition” status is used in this case in Frama-C.

See, resp., https://alt-ergo.ocamlpro.com, http://cvc4.cs.nyu.edu, https://z3.codeplex.com/.

See http://coq.inria.fr/.

Barthe, G., Crespo, J.M., Kunz, C.: Product programs and relational program logics. J. Log. Algebr. Methods Program. 85, 847–859 (2016)MathSciNetCrossRefMATH

Barthe, G., D’Argenio, P.R., Rezk, T.: Secure information flow by self-composition. Math. Struct. Comput. Sci. 21, 1207–1252 (2011)MathSciNetCrossRefMATH

Baudin, P., Bobot, F., Correnson, L., Dargaye, Z.: WP Plugin Manual v1.0 (2016)

Baudin, P., Cuoq, P., Filliâtre, J.C., Marché, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI/ISO C Specification Language (2016). http://frama-c.com/acsl.html

Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: POPL (2004)

Bishop, P.G., Bloomfield, R.E., Cyra, L.: Combining testing and proof to gain high assurance in software: a case study. In: ISSRE (2013)

Burghardt, J., Gerlach, J., Lapawczyk, T.: ACSL by Example (2016). http://www.fokus.fraunhofer.de/download/acsl_by_example

Cok, D.R.: OpenJML: software verification for Java 7 using JML, OpenJDK, and Eclipse. In: F-IDE (2014)

Correnson, L., Signoles, J.: Combining analyses for C program verification. In: Stoelinga, M., Pinger, R. (eds.) FMICS 2012. LNCS, vol. 7437, pp. 108–130. Springer, Heidelberg (2012). doi:10.1007/978-3-642-32469-7_8 CrossRef

10.

Cuoq, P., Monate, B., Pacalet, A., Prevosto, V.: Functional dependencies of C functions via weakest pre-conditions. STTT 13(5), 405–417 (2011)CrossRef

11.

Darvas, A., Müller, P.: Reasoning about method calls in JML specifications. FTfJP (2005)

12.

Hui, Z.W., Huang, S.: A formal model for metamorphic relation decomposition. In: WCSE (2013)

13.

Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. Form. Aspect Comput. 27(3), 573–609 (2015). http://frama-c.com MathSciNetCrossRef

14.

Leino, K.R.M., Müller, P.: Verification of equivalent-results methods. In: Drossopoulou, S. (ed.) ESOP 2008. LNCS, vol. 4960, pp. 307–321. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78739-6_24 CrossRef

15.

Sousa, M., Dillig, I.: Cartesian hoare logic for verifying k-safety properties. In: PLDI (2016)

16.

Weyuker, E.J.: On testing non-testable programs. Comput. J. 25(4), 465–470 (1982)CrossRef

Title: RPP: Automatic Proof of Relational Properties by Self-composition
Authors: Lionel Blatter
Nikolai Kosmatov
Pascale Le Gall
Virgile Prevosto
Publisher: Springer Berlin Heidelberg
Book: Tools and Algorithms for the Construction and Analysis of Systems
Print ISBN: 978-3-662-54576-8

Electronic ISBN: 978-3-662-54577-5

Copyright Year: 2017
DOI: https://doi.org/10.1007/978-3-662-54577-5_22

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner