ECOOP 2025
Mon 30 June - Fri 4 July 2025 Bergen, Norway
Wed 2 Jul 2025 11:06 - 11:27 at Auditorium M003 - Program Analysis and Verification Chair(s): Einar Broch Johnsen

The vulnerability of neural networks to adversarial perturbations has necessitated formal verification techniques that can rigorously certify the quality of neural networks. As the state-of-the-art, branch and bound (BaB) is a ‘‘divide-and-conquer’’ strategy that applies off-the-shelf verifiers to sub-problems for which they perform better. While BaB can identify the sub-problems that are necessary to be split, it explores the space of these sub-problems in a naive ``first-come-first-serve'' manner, thereby suffering from an issue of inefficiency to reach a verification conclusion. To bridge this gap, we introduce an order over different sub-problems produced by BaB, concerning with their different likelihoods of containing counterexamples. Based on this order, we propose a novel verification framework Oliva that explores the sub-problem space by prioritizing those sub-problems that are more likely to find counterexamples, in order to efficiently reach the conclusion of the verification. Even if no counterexample can be found in any sub-problem, it only changes the order of visiting different sub-problem and so will not lead to a performance degradation. Specifically, Oliva has two variants, including $Oliva^{GR}$, a greedy strategy that always prioritizes the sub-problems that are more likely to find counterexamples, and $Oliva^{SA}$, a balanced strategy inspired by simulated annealing that gradually shifts from exploration to exploitation to locate the globally optimal sub-problems. We experimentally evaluate the performance of Oliva on 690 verification problems spanning over 5 models with datasets MNIST and CIFAR10. Compared to the state-of-the-art approaches, we demonstrate the speedup of Oliva for up to 25X in MNIST, and up to 75X in CIFAR10. Logo

Wed 2 Jul

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:45 - 12:30
Program Analysis and VerificationTechnical Papers at Auditorium M003
Chair(s): Einar Broch Johnsen University of Oslo
10:45
21m
Talk
Bottom-up Synthesis of Memory Mutations with Separation Logic
Technical Papers
Kasra Ferdowsi University of California at San Diego, Hila Peleg Technion
11:06
21m
Talk
Efficient Neural Network Verification via Order Leading Exploration of Branch-and-Bound Trees
Technical Papers
Guanqin Zhang University of New South Wales & CSIRO's Data61, Kota Fukuda Kyushu University, Zhenya Zhang Kyushu University, Japan, ‪H M N Dilum Bandara Data61, CSIRO, Shiping Chen Data61 at CSIRO, Australia / UNSW, Australia, Jianjun Zhao Kyushu University, Yulei Sui University of New South Wales
Link to publication Pre-print Media Attached
11:27
21m
Talk
IsaBIL: A Framework for Verifying (In)correctness of Binaries in Isabelle/HOL
Technical Papers
Matt Griffin Imperial College London, Brijesh Dongol University of Surrey, Azalea Raad Imperial College London
11:48
21m
Talk
Reusing Caches and Invariants for Efficient and Sound Incremental Static Analysis
Technical Papers
Mamy Razafintsialonina Université Paris-Saclay, CEA, List, Palaiseau / Sorbonne Université, CNRS, LIP6, Paris, David Bühler Université Paris-Saclay, CEA, List, Palaiseau, Antoine Miné Sorbonne Université, Valentin Perrelle Université Paris-Saclay, CEA, List, Palaiseau, Julien Signoles Université Paris-Saclay, CEA, List
12:09
21m
Talk
RacerF: Lightweight Static Data Race Detection for C Code
Technical Papers
Tomáš Dacík Faculty of Information Technology, Brno University of Technology, Tomas Vojnar Masaryk University
:
:
:
: