VERT: Polyglot Verified Equivalent Rust Transpilation with Large Language Models
This program is tentative and subject to change.
Rust is a programming language that combines memory safety and low-level control, providing C-like performance while guaranteeing the absence of undefined behaviors by default. Rust’s growing popularity has prompted research on correct and idiomatic transpiling of existing code-bases to Rust. Existing work falls into two categories: rule-based and large language model (LLM)-based. While rule-based approaches are theoretically sound, they often yield unidiomatic and unsafe Rust code while targeting a few source languages, hindering maintainability and industrial application. In contrast, LLM-based approaches, while providing no guarantees, are polyglot and typically produce more idiomatic and safe Rust code. In this work, we present VERT, a formally correct, polyglot Rust translator with more idiomatic outputs. VERT supports any language that compiles to Web Assembly. Using the Web Assembly compiler, VERT obtains an oracle Rust program. Leveraging the LLM, VERT generates an idiomatic candidate Rust program. This candidate is verified against the oracle with model-checking to ensure equivalence.
This program is tentative and subject to change.
Mon 17 NovDisplayed time zone: Seoul change
14:00 - 15:30 | |||
14:00 10mTalk | ScaleCirc: Scaling the Analysis over Circom Circuits Research Papers Jinan Jiang The Hong Kong Polytechnic University, Haoran Qin The Hong Kong Polytechnic University, Xiapu Luo Hong Kong Polytechnic University | ||
14:10 10mTalk | Improving NLSAT for Nonlinear Real Arithmetic Research Papers Zhonghan Wang Institute of Software, Chinese Academy of Sciences Pre-print | ||
14:20 10mTalk | Bridging Natural Language and Formal Specification - Automated Translation of Software Requirements to LTL via Hierarchical Semantics Decomposition Using LLMs Research Papers Zhi Ma Xidian University, Xin-Cheng Wen Harbin Institute of Technology, Zhexin Su Xidian University, Xiao Liang Yu National University of Singapore, Cong Tian Xidian University, Shengchao Qin Xidian University, Mengfei Yang China Academy of Space Technology | ||
14:30 10mTalk | Diagnosing Performance Differences in Model Checkers via Runtime-Guided Problem Generation Research Papers Yibo Dong National University of Singapore, Yicong Xu East China Normal University, Wenjing Deng East China Normal University, Yu Chen Chuzhou University, Xiaoyu Zhang East China Normal University, Jianwen Li East China Normal University, China, Chengyu Zhang Loughborough University, Geguang Pu East China Normal University, China | ||
14:40 10mTalk | VERT: Polyglot Verified Equivalent Rust Transpilation with Large Language Models Research Papers Aidan Z.H. Yang Carnegie Mellon University, Yoshiki Takashima Yale Law School, Brandon Paulsen Amazon, Joey Dodds Amazon, Daniel Kroening Amazon | ||
14:50 10mTalk | Agentic Specification Generator for Move Programs Research Papers Yu-Fu Fu Georgia Institute of Technology, Meng Xu University of Waterloo, Taesoo Kim Georgia Institute of Technology Pre-print | ||
15:00 10mTalk | How Big is the Automaton? Certified Lower Bounds on the Size of Presburger DFAs Research Papers Nicolas Amat ONERA - The French Aerospace Lab, Pierre Ganty IMDEA Software Institute, Spain, Alessio Mansutti IMDEA Software Institute | ||
15:10 10mTalk | Non-termination Witnesses and their Validation Research Papers Zsófia Ádám Department of Measurement and Information Systems, Budapest University of Technology and Economics, Paulína Ayaziová Masaryk University, Czechia, Levente Bajczi Budapest University of Technology and Economics, Dirk Beyer LMU Munich, Marek Jankola LMU Munich, Marian Lingsch-Rosenfeld LMU Munich, Jan Strejcek Masaryk University | ||
15:20 10mTalk | PAT-Agent: Autoformalization for Model Checking Research Papers Xinyue Zuo National University of Singapore, Yifan Zhang National University of Singapore, Hongshu Wang National University of Singapore, Yufan Cai National University of Singapore, Zhe Hou Griffith University, Jing Sun School of Computer Science, University of Auckland, Jin Song Dong National University of Singapore | ||