SPLASH 2025
Sun 12 - Sat 18 October 2025 Singapore
co-located with ICFP/SPLASH 2025
Sat 18 Oct 2025 14:30 - 14:45 at Orchid West - Verification 3 Chair(s): KC Sivaramakrishnan

Neural network image classifiers are ubiquitous in many safety-critical applications. However, they are susceptible to adversarial attacks. To understand their robustness to attacks, many local robustness verifiers have been proposed to analyze $\epsilon$-balls of inputs. Yet, existing verifiers introduce a long analysis time or lose too much precision, making them less effective for a large set of inputs. In this work, we propose a new approach to local robustness: group local robustness verification. The key idea is to leverage the similarity of the network computations of certain $\epsilon$-balls to reduce the overall analysis time. We propose BaVerLy, a sound and complete verifier that boosts the local robustness verification of a set of $\epsilon$-balls by dynamically constructing and verifying mini-batches. BaVerLy adaptively identifies successful mini-batch sizes, accordingly constructs mini-batches of $\epsilon$-balls that have similar network computations, and verifies them jointly. If a mini-batch is verified, all its $\epsilon$-balls are proven robust. Otherwise, one $\epsilon$-ball is suspected as not being robust, guiding the refinement. BaVerLy leverages the analysis results to expedite the analysis of that $\epsilon$-ball as well as the analysis of the mini-batch with the other $\epsilon$-balls. We evaluate BaVerLy on fully connected and convolutional networks for MNIST and CIFAR-10. Results show that BaVerLy scales the common one by one verification by 2.3x on average and up to 4.1x, in which case it reduces the total analysis time from 24 hours to 6 hours.

Sat 18 Oct

Displayed time zone: Perth change

13:45 - 15:30
Verification 3OOPSLA at Orchid West
Chair(s): KC Sivaramakrishnan IIT Madras and Tarides
13:45
15m
Talk
Automated Verification of Soundness of DNN Certifiers
OOPSLA
Avaljot Singh UIUC, Yasmin Chandini Sarita UIUC, Charith Mendis University of Illinois at Urbana-Champaign, Gagandeep Singh University of Illinois at Urbana-Champaign; VMware Research
14:00
15m
Talk
Bolt-On Strong Consistency: Specification, Implementation, and Verification
OOPSLA
Nicholas V. Lewchenko University of Colorado Boulder, Gowtham Kaki University of Colorado at Boulder, Bor-Yuh Evan Chang University of Colorado Boulder & Amazon
14:15
15m
Talk
Memory-Safety Verification of Open Programs With Angelic Assumptions
OOPSLA
Gourav Takhar Indian Institute of Technology - Kanpur, Baldip Bijlani Indian Institute of Technology Kanpur, Prantik Chatterjee MathWorks, Akash Lal Microsoft Research, Subhajit Roy IIT Kanpur
14:30
15m
Talk
Mini-Batch Robustness Verification of Deep Neural Networks
OOPSLA
Saar Tzour-Shaday Technion – Israel Institute of Technology, Dana Drachsler Cohen Technion
14:45
15m
Talk
Revamping Verilog Semantics for Foundational VerificationDistinguished Paper
OOPSLA
Joonwon Choi Amazon Web Services, Jaewoo Kim KAIST, Jeehoon Kang FuriosaAI
15:00
15m
Talk
Scalable Equivalence Checking and Verification of Shallow Quantum Circuits
OOPSLA
Nengkun Yu Stony Brook University, USA, Xuan Du Trinh Stony Brook University, Thomas Reps University of Wisconsin-Madison
15:15
15m
Talk
Structural temporal logic for mechanized program verification
OOPSLA
Lef Ioannidis University of Pennsylvania, Yannick Zakowski Inria, Steve Zdancewic University of Pennsylvania, Sebastian Angel University of Pennsylvania