Skip to Main content Skip to Navigation
New interface
Conference papers

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
UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique, IRIF (UMR_8243) - Institut de Recherche en Informatique Fondamentale, 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [19 references]  Display  Hide  Download
Contributor : Yann Regis-Gianas Connect in order to contact the contributor
Submitted on : Friday, December 1, 2017 - 11:43:28 AM
Last modification on : Tuesday, October 25, 2022 - 4:17:24 PM


Files produced by the author(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. ⟨10.1145/3131851.3131870⟩. ⟨hal-01653283⟩



Record views


Files downloads