This page presents the correlating_program tool implementing correlating program generation, as described in our paper, along with detailed experimental results on a series of examples.
As described in our paper, the correlating_program tool only covers the generation of a correlating program, that is, a static interleaving of two programs' instructions in a way that preserves their semantics.
It does not cover the statical analysis of the resulting correlated program. In our experiments, we performed this analysis through abstract interpretation using a slightly patched version of Eran and Yahav's dizy tool.
The correlating_program tool handles an extension of the language described in our paper, in which various arithmetic operators have been added, as well as array values. The approach presented in our paper naturally extends to those changes, and both the algorithm and the proofs have been updated accordingly.
We have chosen to represent the input language using a concrete syntax close to that of the C language. Although its semantics do not exactly match C's, we believe it to be equivalent to the subset of C corresponding to the concrete syntax of our language.
Likewise, our syntactic diff language is designed to resemble the widely-used unified diff format, in order to be immediately readable by those familiar with the latter. Those two languages, however, are fundamentally incompatible, as one is syntactic while the other is purely textual.
While the soundness of our correlating_program is proven in the Coq proof assistant, we evaluate the quality of its output by comparing the results of its analysis by dizy.
Our comparison is done on a selection of difference examples presented as pairs of programs in our source language. For each of those pairs:
All of this is automated by a Python (run_tests.py) script that takes a file listing the tests along with the expected result (equivalent or non-equivalent), and an optional counter-example to the correction of the correlating program.