# TC-Verifier: Trans-Compiler-Based Code Translator Verifier with Model-Checking
## 2 Related Work  
Verification of code translation from one programming language to another has been tackled in very few previous works. On the contrary, the formal verification of code optimization is much more adopted according to the survey undertaken by [PERSON] et al. [2]. Two categories of verification were identified in that survey [2]: (1) Translation verification, which can be defined as verifying equivalence between input and translated code. (2) Translator verification: verifying the correctness of the translator's behavior; hence, all translations should be correct. The latter category is the type of verification within this paper's scope. In the following paragraphs, we summarize the Translator verification methods used in the literature.  
Compiler verification is the most dominant when investigating the previous work of translators' verification. Early work on compiler verification depended on mathematical proofs [2]. Compiler verification was recently tackled using the Coq proof assistant [13], known as the Calculus of Inductive Constructions. This method is considered under translator verification since it represents the compiler model in Coq and formally proves its correctness. This method cannot be easily applied to production compilers because it necessitates that the compilers be written in the language of a proof assistant like Coq. Therefore, proof-based verification might not be applicable for developers not familiar with the mathematical background of Theorem proving. Other methods used symbolic execution to automatically prove the correctness of compilation rules for both the source and target languages [14]. The framework's reliance on symbolic execution can lead to scalability issues, especially for large and complex programs [15].  
[PERSON] et al. [16] used abstract state machines for the incremental verification of compilers through bisimulation of two abstract state machines (ASMs) to verify the correct mapping between source and target languages. They formalized and verified the memory mapping of the initial versions with ASMs and discussed their extensibility for the next increments. The approach is demonstrated through the agile implementation and verification of a Sather-K compiler generating MIPS assembly language.  
Most of the investigated literature in the context of translators' verification depended on formal proofs or ASMs like [PERSON] et al. [16]. The formal proof approach is very complex and needs to be revisited or reapplied after updating the translator. The ASM idea of [PERSON] et al. [16] does not apply to the kind of trans-compilers we are interested in verifying. The trans-compilers [5; 6; 17] depend on the translation rules inside the parser generator written by developers. These trans-compilers do not use the mapping between the abstract syntax trees of the source and target languages like the compiler used by [PERSON] et al. [16]. Therefore, inspired by the work undertaken in [16], we decided to introduce TC-Verifier to model the behavior of the parser-based trans-compilers using state machines instead of the ASMs of the languages. The modeled compiler will then be verified using model-checking. This model-checking step will verify the translator's correctness and point out its unverified or incorrect translations.