APSEC 2024
Tue 3 - Fri 6 December 2024 China
Fri 6 Dec 2024 14:00 - 14:30 at Room 2 (Xiangshan Ballroom) - Session (19) Chair(s): Ke Yu

Neural network verification, particularly verification of robustness properties, has received much research attention. However, many existing verification methods overlook the influence of floating-point rounding errors in the deployed neural networks, resulting in unsound verification outcomes. In this paper, we propose a sound robustness verification approach aiming at overcoming this limitation. Our method utilizes real-number intervals to approximate floating-point arithmetic and abstracts floating-point neural networks into equivalent networks using real-number interval arithmetic semantics, thereby effectively taking into account for floating-point rounding errors. We subsequently employ exact MILP formulations to verify robustness over these abstracted networks. We introduce FMIPVerify, a dedicated verification tool tailored to ensure the soundness of floating-point neural network verification. Experimental results demonstrate that FMIPVerify significantly improves the robustness verification ability in floating-point ReLU neural networks compared to established complete methods like MIPVerify.

Fri 6 Dec

Displayed time zone: Beijing, Chongqing, Hong Kong, Urumqi change

14:00 - 15:30
14:00
30m
Talk
Sound Floating-Point Neural Network Verification with MILP
Technical Track
Shifu Yang College of Computer, National University of Defense Technology, Changsha, China, Liqian Chen National University of Defense Technology, Banghu Yin College of Computer, National University of Defense Technology, Changsha, China, Minghao Li College of Computer, National University of Defense Technology, Changsha, China, Yuan Zhou University of Oxford, Ji Wang National University of Defense Technology
14:30
30m
Talk
Parallel symbolic execution for smart contracts with load balancing
Technical Track
Xiaorui Nie hbuniexiaorui@163.com, Meng Wang Hebei university
15:00
20m
Talk
Designing distributed systems using SAT solvers
ERA - Early Research Achievements