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

This program is tentative and subject to change.

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

Designing algorithms for complex problems as certifying algorithms is an important approach to ensure correctness of computational results. Instead of producing output $y$ for an input $x$, a certifying algorithm produces for $x$ not only $y$ but also a witness $w$. The witness $w$ (also called certificate) can now be used to check that $y$ is indeed the correct output for input $x$. Witnesses and their validation also exist in the area of automatic software verification, and a large number of tools support verification witnesses (SV-COMP reports 62 verifiers producing witnesses and 18 tools for witness validation). In 2023, a new version 2.0 of the witness format for software verification was introduced to overcome several problems with the previous format, and this new format is now widely supported. However, there is no format with a clear definition and semantics for witnesses of non-termination. This paper closes this gap by presenting an extension of the witness format 2.0 to support program non-termination. Besides explaining the design of this extension, we describe various approaches to generate and validate non-termination witnesses. We also give an overview of current tool support of the extended format, i.e., the verifiers that can generate non-termination witnesses and the witness validators able to analyze these witnesses. Finally, we present an experimental evaluation showing the performance of these tools on program-termination tasks of SV-COMP~2025.

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