A Mechanically Checked Generation of Correlating Programs Directed by Structured Syntactic Differences

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, Inria Paris-Rocquencourt, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique : UMR7126
Abstract : We present a new algorithm for the construction of a correlating program from the syntactic difference between the original and modified versions of a program. This correlating program exhibits the semantics of the two input programs and can then be used to compute their semantic differences, following an approach of Partush and Yahav [12]. We show that Partush and Yahav's correlating program is unsound on loops that include an early exit. Our algorithm is defined on an imperative language with while-loops, break, and continue. To guarantee its correctness, it is formalized and mechanically checked within the Coq proof assistant. On a series of examples, we experimentally find that the static analyzer dizy is at least as precise on our correlating program as on Partush and Yahav's.
Type de document :
Communication dans un congrès
Automated Technology for Verification and Analysis, Oct 2015, Shanghai, China. Automated Technology for Verification and Analysis, Lecture Notes in Computer Science 9364, Springer 2015, 9364, 2015, Lecture Notes in Computer Science. 〈10.1007/978-3-319-24953-7_6〉
Liste complète des métadonnées

Littérature citée [15 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01238704
Contributeur : Yann Regis-Gianas <>
Soumis le : dimanche 6 décembre 2015 - 21:37:14
Dernière modification le : dimanche 13 janvier 2019 - 15:32:17
Document(s) archivé(s) le : samedi 29 avril 2017 - 06:56:34

Fichier

root.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Thibaut Girka, David Mentré, Yann Régis-Gianas. A Mechanically Checked Generation of Correlating Programs Directed by Structured Syntactic Differences. Automated Technology for Verification and Analysis, Oct 2015, Shanghai, China. Automated Technology for Verification and Analysis, Lecture Notes in Computer Science 9364, Springer 2015, 9364, 2015, Lecture Notes in Computer Science. 〈10.1007/978-3-319-24953-7_6〉. 〈hal-01238704〉

Partager

Métriques

Consultations de la notice

296

Téléchargements de fichiers

174