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

This program is tentative and subject to change.

Tue 18 Nov 2025 11:20 - 11:30 at Grand Hall 3 - Formal Method & Verification 2

Neural Network Verification has made significant progress in recent years, with the development of numerous verification techniques and tools. However, the field still lacks high-quality benchmarks for systematically evaluating and improving these tools. As verification techniques advance, many existing benchmarks have become too trivial, while the harder ones often remain unsolvable. Several recent efforts have attempted to address this gap, typically by retraining or distilling neural networks to create new benchmarks. However, such approaches are computationally expensive and often produce benchmarks with unknown or unverifiable ground truth. In this paper, we introduce ReluSplitter, an automatic benchmark generation tool for DNN verifiers. ReluSplitter takes existing verification benchmarks as input and strategically destabilizes stable neurons to increase verification difficulty. This transformation is semantics-preserving by construction: every ReluSplitter-generated benchmark is guaranteed to have exactly the same ground truth as the original benchmark. This makes ReluSplitter particularly valuable for assessing verifier correctness and performance. Our evaluation demonstrates that ReluSplitter can significantly increase the difficulty of existing benchmarks, effectively challenging state-of-the-art DNN verifiers. We believe ReluSplitter offers a practical and principled way to generate benchmarks with tunable difficulty and verifiable ground truth, contributing a much-needed resource for the neural network verification community.

This program is tentative and subject to change.

Tue 18 Nov

Displayed time zone: Seoul change

11:00 - 12:30
Formal Method & Verification 2Research Papers at Grand Hall 3
11:00
10m
Talk
SMTgazer: Learning to Schedule SMT Algorithms via Bayesian Optimization
Research Papers
Chuan Luo Beihang University, Shaoke Cui Beihang University, Jianping Song Beihang University, Xindi Zhang State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, China, Wei Wu Central South University; Xiangjiang Laboratory, Chanjuan Liu Dalian University of Technology, Shaowei Cai Institute of Software at Chinese Academy of Sciences, Chunming Hu Beihang University
11:10
10m
Talk
Efficient and Verifiable Proof Logging for MaxSAT Solving
Research Papers
Raoul van Doren ETH Zurich, Timos Antonopoulos Yale University, Ruzica Piskac Yale University
11:20
10m
Talk
Destabilizing Neurons to Generate Challenging Neural Network Verification Benchmarks
Research Papers
Linhan Li , ThanhVu Nguyen George Mason University
11:30
10m
Talk
RELIA: Accelerating Analysis of Cloud Access Control Policies
Research Papers
Dan Wang Xi'an Jiaotong University, Peng Zhang Xi'an Jiaotong University, Zhenrong Gu Xi'an Jiaotong University, Weibo Lin Huawei Cloud, Shibiao Jiang Huawei Cloud, Zhu He Huawei Cloud, Xu Du Huawei Cloud, Longfei Chen Huawei Cloud, Jun Li Huawei, Xiaohong Guan Xi'an Jiaotong University
11:40
10m
Talk
Evolution-Aware Heuristics for GR(1) Realizability Checking
Research Papers
Dor Ma'ayan Tel Aviv University, Shahar Maoz Tel Aviv University, Jan Oliver Ringert Bauhaus-University Weimar
11:50
10m
Talk
Programmers’ Visual Attention on Function Call Graphs During Code Summarization
Research Papers
Samantha McLoughlin Vanderbilt University, Zachary Karas Vanderbilt University, Robert Wallace University of Notre Dame, Aakash Bansal Louisiana State University, Collin McMillan University of Notre Dame, Yu Huang Vanderbilt University
12:00
10m
Talk
LLM-Assisted Synthesis of High-Assurance C Programs
Research Papers
Prasita Mukherjee Purdue University, Minghai Lu Purdue University, Benjamin Delaware Purdue University
Pre-print
12:10
10m
Talk
Faster Runtime Verification during Testing via Feedback-Guided Selective Monitoring
Research Papers
Shinhae Kim Cornell University, Saikat Dutta Cornell University, Owolabi Legunsen Cornell University
12:20
10m
Talk
Uncovering Discrimination Clusters: Quantifying and Explaining Systematic Fairness Violations
Research Papers
Ranit Debnath Akash University of Illinois Chicago, Ashish Kumar Pennsylvania State University, Verya Monjezi University of Texas at El Paso, Ashutosh Trivedi University of Colorado Boulder, Gang (Gary) Tan Pennsylvania State University, Saeid Tizpaz-Niari University of Illinois Chicago