# TC-Verifier: Trans-Compiler-Based Code Translator Verifier with Model-Checking
## 4 Results and Discussion
### Discussion  
The verification results of the four tested statements checked by 67 symbolic queries show the following: (1) The common unverified cases are cases where there is no direct correspondence in the target language. For example, no equivalence to the where clause used in function and class declarations in the Swift language. Similarly, access modifiers like fileprivate and open access modifiers do not have any direct equivalent in Java. (2) Other than the no direct equivalent cases, there were cases that Java had an equivalent either directly or with a workaround, but were not covered by the compiler, like the usage of the throw keyword and the usage of the generic parameter clause in the class declaration. These cases show the importance of verification with model checking as it can help compiler developers to add the unverified parts that can be implemented to improve the trans-compiler. For the parts that have no direct equivalence, integration with fine-tuned LLMs can be the next step. While this paper proposes the augmentation of trans-compilers with LLMs to fill the identified translation gaps, the formal verification of LLMs themselves presents a complex challenge. Future research could explore the feasibility of formally verifying LLMs within this context.  
The main limitations of the presented approach for verifying trans-compilers can be summarized as follows: (1) The hierarchical and recursive nature of the grammar rules and productions makes it sometimes impossible to complete a state machine representation of a certain rule or statement until all other related rules are modeled. This made us ignore some parts in the modeled rules and postpone them to upcoming modeling rounds, like ignoring the variable declaration with initialization, for example. (2) The modeling process that converts the translator's behavior to a state machine is performed manually. Therefore, it must be learned by the TC-Verifier users. The modeling process is considered easy and user-friendly for trans-compiler developers. However, it can take more time for users who are not familiar with the translation process behind the translator to be verified. Automating this process will boost the time complexity of the modeling process and eliminate the need to learn manual modeling. (3) The UPPaal model checker used in the presented architecture does not support string variables, and therefore all the string variables used in the translator had to be encoded to be modeled in the Uppaal tool. (4) Migrating the TC-Verifier to be used for different source and target languages implies the cost of modeling the state machines for the new translation processes. The symbolic queries can be reused for the same source language even if the output language is changed. If the source language  
\begin{table}
\begin{tabular}{c c c c c} \hline \hline  & \multicolumn{2}{c}{**BLEU Reference Translation**} & \multicolumn{2}{c}{**TC-Verifier**} \\ \cline{2-5}  & **Translation 1** & **Translation 2** & **Translation 3** & **Trans-Compiler** \\ \hline Array declaration & 52.54 & 31.34 & 88.01 & 100.00 & Verified translation \\ \hline \hline \end{tabular}
\end{table}
Table 12: BLEU scores for different reference translations VS TC-Verifier result.  
is changed, new queries must be defined. However, queries can be automatically retrieved either using an LLM as we presented in the approach or by an automated script that can directly retrieve the symbolic queries from the XML of the state machine.