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

This program is tentative and subject to change.

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

Automating the translation of natural language (NL) software requirements into formal specifications remains a critical challenge in scaling formal verification practices to industrial settings, particularly in safety-critical domains. Existing approaches, both rule-based and learning-based, face significant limitations. While large language models (LLMs) like GPT-4o demonstrate proficiency in semantic extraction, they still encounter difficulties in addressing the complexity, ambiguity, and logical depth of real-world industrial requirements. In this paper, we propose \textbf{Req2LTL}, a modular framework that bridges NL and Linear Temporal Logic (LTL) through a hierarchical intermediate representation called \textit{OnionL}. \textbf{Req2LTL} leverages LLMs for semantic decomposition and combines them with deterministic rule-based synthesis to ensure both syntactic validity and semantic fidelity. Our comprehensive evaluation demonstrates that \textbf{Req2LTL} achieves 88.4% semantic accuracy and 100% syntactic correctness on real-world aerospace requirements, significantly outperforming existing methods.

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