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 : vendredi 25 mai 2018 - 12:02:06
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

290

Téléchargements de fichiers

101