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

This program is tentative and subject to change.

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

Runtime verification (RV) uses monitors, which are dynamically created based on formal specifications (specs), to check running programs against specs. RV of passing tests in many open-source projects found hundreds of new bugs. But, high overheads make it hard to use RV for testing in practice. We propose Valg, the first on-the-fly selective RV technique for testing, and the first to use reinforcement learning (RL) to speed up RV. Valg leverages a recent finding: 99.87% of monitors are redundant for testing; they wastefully re-check unique traces—sequences of events, e.g., method calls—that the other necessary 0.13% already checked. Valg uses feedback about redundancy of prior monitors and events to selectively monitor only necessary ones subsequently. A key idea in Valg is our novel formulation of selective monitor creation as a two-armed bandit RL problem that rewards necessary monitors, and penalizes redundant ones. We implement Valg for Java and compare it with state-of-the-art RV tools on one revision each of 64 open-source projects. With default RL hyperparameters, Valg is up to 20.2x and 555.6x faster than JavaMOP and TraceMOP, respectively. For example, Valg takes only 54.8 minutes in total to monitor three projects where TraceMOP takes 3.02 days in total. Valg finds 99.6% of JavaMOP and TraceMOP’s spec violations, but it only checks 76.7% of their unique traces on average. After tuning hyperparameters, Valg checks 95.1% of unique traces on average with little loss in speed. Using tuned hyperparameters from one revision “into the future” as code evolves preserves Valg’s high rate of checked unique traces and speedups, without needing frequent re-tuning.

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