Renaming Global Variables in C Mechanically Proved Correct
Programming Languages
2016-07-11 v1
Abstract
Most integrated development environments are shipped with refactoring tools. However, their refactoring operations are often known to be unreliable. As a consequence, developers have to test their code after applying an automatic refactoring. In this article, we consider a refactoring operation (renaming of global variables in C), and we prove that its core implementation preserves the set of possible behaviors of transformed programs. That proof of correctness relies on the operational semantics of C provided by CompCert C in Coq.
Keywords
Cite
@article{arxiv.1607.02226,
title = {Renaming Global Variables in C Mechanically Proved Correct},
author = {Julien Cohen},
journal= {arXiv preprint arXiv:1607.02226},
year = {2016}
}
Comments
In Proceedings VPT 2016, arXiv:1607.01835