FormaliSE 2023
Dates to be announced Melbourne, Australia
co-located with ICSE 2023
Sun 14 May 2023 11:30 - 12:00 at Meeting Room 102 - Synthesis and AI Chair(s): Mark Utting

Deep Neural Networks (DNNs) have become a popular instrument for solving various real-world problems. DNNs’ sophisticated structure allows them to learn complex representations and features. For this reason, Binary Neural Networks (BNNs) are widely used on edge devices, such as microcomputers. However, architecture specifics and floating-point number usage result in an increased computational operations complexity. Like other DNNs, BNNs are vulnerable to adversarial attacks; even a small perturbation to the input set may lead to an errant output. Unfortunately, only a few approaches have been proposed for verifying BNNs. This paper proposes a novel approach to verify BNNs on continuous input space using star reachability analysis. Our approach can compute both exact and overapproximate reachable sets of BNNs with Sign activation functions and use them for verification. The proposed approach is also efficient in constructing a complete set of counterexamples in case a network is unsafe. We implemented our approach in NNV, a neural network verification tool for DNNs and learning-enabled Cyber-Physical Systems. The experimental results show that our star-based approach is less conservative, more efficient, and scalable than the recent SMT-based method implemented in Marabou. We also provide a comparison with a quantization-based tool EEVBNN.

Sun 14 May

Displayed time zone: Hobart change

11:00 - 12:30
Synthesis and AIFormaliSE 2023 at Meeting Room 102
Chair(s): Mark Utting The University of Queensland
11:00
30m
Talk
Goal Controller Synthesis for Self-Adaptive Systems
FormaliSE 2023
Radu Calinescu University of York, UK, Genaína Nunes Rodrigues University of Brasília
11:30
30m
Paper
Verifying Binary Neural Networks on Continuous Input Space using Star Reachability
FormaliSE 2023
Mykhailo Ivashchenko University of Nebraska-Lincoln, Sung Woo Choi , Luan Nguyen University of Pennsylvania, Hoang-Dung Tran Vanderbilt University
12:00
30m
Paper
Explainable Human-Machine Teaming using Model Checking and Interpretable Machine Learning
FormaliSE 2023
Marcello Bersani Politecnico di Milano, Italy, Matteo Camilli Politecnico di Milano, Livia Lestingi DEIB, Politecnico di Milano, Raffaela Mirandola Politecnico di Milano, Matteo Rossi Politecnico di Milano