NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems

Author(s)

Hoang-Dung Tran, University of Nebraska
Xiaodong Yang, University of Nebraska
Diego Manzanas Lopez, University of Nebraska
Patrick Musau, University of Nebraska
Luan Viet Nguyen, University of DaytonFollow
Weiming Xiang, Augusta University
Stanley Bak, Stony Brook University
Taylor T. Johnson, University of NebraskaFollow

Document Type

Article

Publication Date

2020

Publication Source

Computer Aided Verification (CAV 2020), PT I

Abstract

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 overapproximate 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.

Inclusive pages

3-17

ISBN/ISSN

0302-9743

Document Version

Published Version

Comments

This open-access article is provided for download in compliance with the publisher’s policy on self-archiving. To view the version of record, use the DOI: https://doi.org/10.1007/978-3-030-53288-8_1

Publisher

Springer-Verlag Berlin

Volume

12224

Peer Reviewed

yes

eCommons Citation

Tran, Hoang-Dung; Yang, Xiaodong; Lopez, Diego Manzanas; Musau, Patrick; Nguyen, Luan Viet; Xiang, Weiming; Bak, Stanley; and Johnson, Taylor T., "NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems" (2020). Computer Science Faculty Publications. 198.
https://ecommons.udayton.edu/cps_fac_pub/198