# TC-Verifier: Trans-Compiler-Based Code Translator Verifier with Model-Checking
## 3 Methodology
### TC-Verifier Architecture  
This paper introduces TC-Verifier for applying the Uppaal model checker to a trans-compiler-based translator. The overall architecture of TC-Verifier is given in Figure 1.  
Any programming language has specifications and Grammar rules that define the correct syntax of the language. The trans-compilers [5; 6; 17] use a parser generator that walks the parse tree of the input language. Then, the translator developer defines translation rules between the source and input language and writes these rules in the parser walker of the input language. Whenever a source code is given to the translator, it is parsed, and the parser walker is triggered with the translation rules written inside. Eventually, the target code is generated. This part is number one in the architecture Figure 1.  
In the second part of TC-Verifier, the translator developer iterates over the source language grammar and checks the translation rules for each statement in the source language grammar. The developer manually models these translation rules as states and transitions in the model checker Uppaal. If a rule or a production in the source grammar does not have a translation rule to the output language, it is modeled as a deadlock in the state machine. If a rule is covered but produces, in some cases, an incomplete or un-compilable code statement according to the output language Grammar, it is also represented as a deadlock in the state machine.  
In step three, since the Uppaal model checker does not support string variables, we use a string-to-integers encoder script to encode all string variables needed to model the translation processes. The fourth step is running the state machine in the Uppaal model checker, and then Uppaal generates the XML format of the state machine model in step five.  
Figure 1: The architecture of TC-Verifier: Trans-compiler-based translators formal verifier using the Uppaal model checker and chatGPT4 for query generation.  
In step six, we use prompt engineering with few shot learning to tune GPT4 to generate the query file needed to verify the state machine produced by Uppaal. Prompt engineering is the process of crafting inputs or prompts for language models to guide them toward desired responses [26; 27; 28]. Few-shot learning is a type of prompt engineering that involves providing the model with a few example prompts and answers within the input. This technique helps the model understand task patterns and improve response quality with minimal data [27]. This process saves time in the manual writing of the properties and queries as they must be written in the model-checker-specific syntax.  
When the query file in step seven is ready, the verifier runs all the queries using an automated script, as shown in step eight. A result verified or not verified for each query is given in step nine. A proof trace is also given for the unverified cases. The output shows the verified and unverified paths for each code statement modeled by the model checker. In step ten, we implemented the automatic script to generate the result of the verification in the form of a list containing the query, the comment explaining the query and the result verified or not verified.