ASE 2025
Sun 16 - Thu 20 November 2025 Seoul, South Korea

This program is tentative and subject to change.

Mon 17 Nov 2025 14:40 - 14:50 at Grand Hall 3 - Formal Method & Verification 1

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 Nov

Displayed time zone: Seoul change

14:00 - 15:30
Formal Method & Verification 1Research Papers at Grand Hall 3
14:00
10m
Talk
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
10m
Talk
Improving NLSAT for Nonlinear Real Arithmetic
Research Papers
Zhonghan Wang Institute of Software, Chinese Academy of Sciences
Pre-print
14:20
10m
Talk
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
10m
Talk
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
10m
Talk
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
10m
Talk
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
10m
Talk
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
10m
Talk
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
10m
Talk
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