Skip to Main content Skip to Navigation
Conference papers

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.
Document type :
Conference papers
Complete list of metadata

Cited literature [15 references]  Display  Hide  Download
Contributor : Yann Regis-Gianas Connect in order to contact the contributor
Submitted on : Sunday, December 6, 2015 - 9:37:14 PM
Last modification on : Friday, January 21, 2022 - 3:22:25 AM
Long-term archiving on: : Saturday, April 29, 2017 - 6:56:34 AM


Files produced by the author(s)




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. ⟨10.1007/978-3-319-24953-7_6⟩. ⟨hal-01238704⟩



Record views


Files downloads