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)

1 MERCE-France - Mitsubishi Electric R&D Centre Europe [France]
2 PPS - Preuves, Programmes et Systèmes
3 PI.R2 - Design, study and implementation of languages for proofs and programs

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.

Domaines: Langage de programmation [cs.PL]

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⟩