Verifiable Semantic Difference Languages

Thibaut Girka 1, 2, 3 David Mentré 1 Yann Régis-Gianas 2, 3
3 PI.R2 - Design, study and implementation of languages for proofs and programs
PPS - Preuves, Programmes et Systèmes, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique, Inria de Paris
Abstract : Program differences are usually represented as textual differences on source code with no regard to its syntax or its semantics. In this paper, we introduce semantic-aware difference languages. A difference denotes a relation between program reduction traces. A difference language for the toy imperative programming language Imp is given as an illustration. To certify software evolutions, we want to mechanically verify that a difference correctly relates two given programs. Product programs and correlating programs are effective proof techniques for relational reasoning. A product program simulates, in the same programming language as the compared programs, a well-chosen interleaving of their executions to highlight a specific relation between their reduction traces. While this approach enables the use of readily-available static analysis tools on the product program, it also has limitations: a product program will crash whenever one of the two programs under consideration crashes, thus making it unsuitable to characterize a patch fixing a safety issue. We replace product programs by correlating oracles which need not be expressed in the same programming language as the compared programs. This allows designing correlating oracle languages specific to certain classes of program changes and capable of relating crashing programs with non-crashing ones. Thanks to oracles, the primitive differences of our difference language on Imp can be assigned a verifiable semantics. Besides, each class of oracles comes with a specific proof scheme which simplifies relational reasoning for a well-specified class of relations. We also prove that our framework is at least as expressive as several Relational Hoare Logic variants by encoding them as correlating oracles, (re)proving sound-ness of those variants in the process. The entirety of the framework as well as its instantiations have been defined and proved correct using the Coq proof assistant.
Type de document :
Communication dans un congrès
International Symposium on Principles and Practice of Declarative Programming, Oct 2017, Namur, Belgium. 2017, 〈10.1145/3131851.3131870〉
Liste complète des métadonnées

Littérature citée [23 références]  Voir  Masquer  Télécharger
Contributeur : Yann Regis-Gianas <>
Soumis le : vendredi 1 décembre 2017 - 11:43:28
Dernière modification le : jeudi 11 janvier 2018 - 06:28:03


Fichiers produits par l'(les) auteur(s)




Thibaut Girka, David Mentré, Yann Régis-Gianas. Verifiable Semantic Difference Languages. International Symposium on Principles and Practice of Declarative Programming, Oct 2017, Namur, Belgium. 2017, 〈10.1145/3131851.3131870〉. 〈hal-01653283〉



Consultations de la notice


Téléchargements de fichiers