NNV swMATH ID: 32539 Software Authors: Hoang-Dung Tran, Xiaodong Yang, Diego Manzanas Lopez, Patrick Musau, Luan Viet Nguyen, Weiming Xiang, Stanley Bak, Taylor T. Johnson Description: NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems. This paper presents the Neural Network Verification (NNV) software tool, a set-based verification framework for deep neural networks (DNNs) and learning-enabled cyber-physical systems (CPS). The crux of NNV is a collection of reachability algorithms that make use of a variety of set representations, such as polyhedra, star sets, zonotopes, and abstract-domain representations. NNV supports both exact (sound and complete) and over-approximate (sound) reachability algorithms for verifying safety and robustness properties of feed-forward neural networks (FFNNs) with various activation functions. For learning-enabled CPS, such as closed-loop control systems incorporating neural networks, NNV provides exact and over-approximate reachability analysis schemes for linear plant models and FFNN controllers with piecewise-linear activation functions, such as ReLUs. For similar neural network control systems (NNCS) that instead have nonlinear plant models, NNV supports over-approximate analysis by combining the star set analysis used for FFNN controllers with zonotope-based analysis for nonlinear plant dynamics building on CORA. We evaluate NNV using two real-world case studies: the first is safety verification of ACAS Xu networks and the second deals with the safety verification of a deep learning-based adaptive cruise control system. Homepage: https://arxiv.org/abs/2004.05519 Source Code: https://github.com/verivital/nnv/ Keywords: Systems and Control; arXiv_eess.SY; arXiv_Machine Learning; arXiv_cs.LG; Deep Neural Networks; Neural Network Verification Related Software: Reluplex; VERIFAI; Marabou; MPT; MNIST; NeuralCDE; torchcde; Diffrax; JuliaReach; nnenum; Verisig; GoTube; ANODE; NNVODE; Flow*; ReachNN; SpaceEx; torchdiffeq; SqueezeDet; Easychair Cited in: 5 Publications Standard Articles 1 Publication describing the Software Year NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems Hoang-Dung Tran, Xiaodong Yang, Diego Manzanas Lopez, Patrick Musau, Luan Viet Nguyen, Weiming Xiang, Stanley Bak, Taylor T. Johnson 2020 all top 5 Cited by 20 Authors 2 Johnson, Taylor T. 2 Manzanas Lopez, Diego 2 Musau, Patrick 1 Bak, Stanley 1 Chen, Taolue 1 Fang, Wang 1 Guan, Ji 1 Hamilton, Nathaniel P. 1 Jia, Kai 1 Liu, Zhiming 1 Nguyen, Luan Viet 1 Pal, Neelanjana 1 Rinard, Martin C. 1 Tran, Hoang-Dung 1 Woodcock, James C. P. 1 Xiang, Weiming 1 Yang, Xiaodong 1 Ying, Mingsheng 1 Zeng, Xia 1 Zhao, Hengjun Cited in 1 Serial 2 Formal Aspects of Computing Cited in 2 Fields 5 Computer science (68-XX) 1 Numerical analysis (65-XX) Citations by Year