SAS 2022
Mon 5 - Wed 7 December 2022 Auckland, New Zealand
co-located with SPLASH 2022
Mon 5 Dec 2022 13:30 - 14:00 at AMRF Auditorium - Numerical Static Analyses Chair(s): Isabella Mastroeni

Deep neural networks (DNNs) have achieved remarkable performance in a myriad of complex tasks. However, lack of robustness and black-box nature hinder their deployment in safety-critical systems. A large number of testing and formal verification techniques have been proposed recently, aiming to provide quality assurance for DNNs. Generally speaking, testing is a fast and simple way to disprove—but not to prove—certain properties of DNNs, while formal verification can provide correctness guarantees but often suffers from scalability and efficiency issues. In this work, we present a novel methodology, CLEVEREST, to accelerate formal verification of DNNs by synergistically combining testing and formal verification techniques based on the counterexample guided abstraction refinement (CEGAR) framework. We instantiate our methodology by leveraging CEGAR-NN, which is a CEGAR-based neural network verification method, and a representative adversarial attack method for testing. We conduct extensive experiments on the widely-used ACAS Xu DNN benchmark. The experimental results show that the testing can effectively reduce the usage of formal verification in the check-refine loop, hence significantly improves the efficiency.

Mon 5 Dec

Displayed time zone: Auckland, Wellington change

13:30 - 15:00
Numerical Static AnalysesSAS at AMRF Auditorium
Chair(s): Isabella Mastroeni University of Verona, Italy
13:30
30m
Talk
CLEVEREST: Accelerating CEGAR-based Neural Network Verification via Adversarial AttacksVirtual
SAS
Zhe Zhao ShanghaiTech University, Yedi Zhang ShanghaiTech University, Guangke Chen ShanghaiTech University, Fu Song ShanghaiTech University, Taolue Chen Birkbeck University of London, Jiaxiang Liu Shenzhen University
14:00
30m
Talk
Boosting Robustness Verification of Semantic Feature Neighborhoods
SAS
Anan Kabaha Technion, Israel Institute of Technology, Dana Drachsler Cohen Technion
14:30
30m
Talk
Lifting Numeric Relational Domains to Algebraic Data Types
SAS
Santiago Bautista Univ Rennes, Inria, CNRS, IRISA, Thomas P. Jensen INRIA Rennes, Benoît Montagu Inria
Pre-print File Attached