.png){kind=icon}
返回
TC-Verifier: Trans-Compiler-Based Code Translator Verifier with Model-Checking
.png){kind=icon}
PRE
AI
DOI：10.3390-asi8030060.png)
.png){kind=icon}
原文求助.png){kind=icon}
分享.png){kind=icon}
收藏
摘要
En 中文
代码到代码的翻译是软件工程中的一个关键领域，越来越多地利用转换编译器在高层次语言之间进行翻译。传统上，此类翻译的保真度一直采用BLEU分数进行评估，该指标主要衡量生成输出与真实结果之间的标记相似度。然而，这一指标未能评估翻译过程背后的方法学，并且仅评估了被测试的翻译。为了弥合这一差距，本文引入了一种创新架构“TC-Verifier”，以正式采用Uppaal模型检查器来验证基于转换编译器的代码翻译器。我们将所提出的架构应用于一个在Swift和Java之间进行翻译的转换编译器，从而为翻译过程的已验证和未验证方面提供了见解。我们的发现阐明了在代码翻译中使用模型检测进行形式化验证的优点和局限性。值得注意的是，所考察的转换编译器在建模的语法规则和产生式上达到了50.74%的验证成功率。本研究强调了基于转换编译器的翻译中的差距，并指出这些差距可能在未来的工作中通过整合大型语言模型（LLMs）来潜在解决。
Keyword:
code-to-code translation
trans-compiler
formal verification
Uppaal Model-checker
BLEU score
期刊
IF:
3.7
论文数:
976
被引数:
1.9K
机构
引用论文
Zhu, M.; Karim, M.; Lourentzou, I.; Yao, D. Semi-Supervised Code Translation Overcoming the Scarcity of Parallel Code Data. In Proceedings of the ASE ’24—39th IEEE/ACM International Conference on Automated Software Engineering, Sacramento, CA, USA, 27 October–1 November 2024; pp. 1545–1556. [Google Scholar] [CrossRef]朱, M.; 卡里姆, M.; 劳伦佐, I.; 姚, D. 半监督代码翻译克服平行代码数据的稀缺. 在第39届IEEE/ACM国际自动化软件工程会议论文集ASE ’24, 美国加利福尼亚州萨克拉门托, 2024年10月27日–11月1日; 第1545–1556页. [Google Scholar] [CrossRef].png)
IF0
PREAI
分享收藏Steinhöfel, D.; Hähnle, R. Modular, correct compilation with automatic soundness proofs. In Leveraging Applications of Formal Methods, Verification and Validation. Modeling. Proceedings of the 8th International Symposium, ISoLA 2018, Limassol, Cyprus, 5–9 November 2018; Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Springer: Cham, Switzerland, 2018; Volume 11244, pp. 424–447. [Google Scholar] [CrossRef]Steinhöfel, D.; Hähnle, R. 模块化、正确的编译与自动完备性证明。载于《形式方法的应用、验证与确认：建模》。2018年国际 Symposium ISoLA 第8次会议 proceedings，2018年11月5日至9日，塞浦路斯利马索尔；计算机科学讲义（包括子系列人工智能讲义与生物信息学讲义）；施普林格出版社：瑞士楚姆，2018年，卷11244，第424-447页。[Google Scholar][CrossRef]
IF0
PREAI
分享收藏
Mahmoud, A.T.; Muhammad, A.A.; Yousef, A.H.; Medhat, W.; Zayed, H.H.; Selim, S. Compiler-based Web Services code conversion model for different languages of mobile application. In Proceedings of the 1st International Conference of Intelligent Methods, Systems and Applications, IMSA 2023, Giza, Egypt, 15–16 July 2023; pp. 464–469. [Google Scholar] [CrossRef]Mahmoud, A.T.; Muhammad, A.A.; Yousef, A.H.; Medhat, W.; Zayed, H.H.; Selim, S. 基于编译器的移动应用程序不同语言Web服务代码转换模型。发表于2023年第一届智能方法、系统与应用国际会议（IMSA 2023），埃及吉萨，2023年7月15–16日；第464–469页。[Google Scholar] [CrossRef]
IF0
PREAI
分享收藏
Zimmermann, W.; Kühn, T.; Sabinus, E.; Weißbach, M. Small Step Incremental Verification of Compilers. In Proceedings of the Rigorous State-Based Methods: 10th International Conference, ABZ 2024, Bergamo, Italy, 25–28 June 2024; Springer: Cham, Switzerland; pp. 262–269. [Google Scholar] [CrossRef]Zimmermann, W.; Kühn, T.; Sabinus, E.; Weißbach, M. 编译器的小步增量验证。载于《基于严谨状态的方法：第10届国际会议ABZ 2024论文集》，意大利贝加莫，2024年6月25–28日；施普林格出版社：瑞士楚格；第262–269页。[Google Scholar][CrossRef]
IF0
PREAI
分享收藏
查看更多内容