@inproceedings{e96ebc54a4884c6cb933a502614a716d,
title = "NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems",
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 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.",
keywords = "Autonomy, Cyber-physical systems, Machine learning, Neural networks, Verification",
author = "Tran, {Hoang Dung} and Xiaodong Yang and {Manzanas Lopez}, Diego and Patrick Musau and Nguyen, {Luan Viet} and Weiming Xiang and Stanley Bak and Johnson, {Taylor T.}",
note = "Funding Information: The material presented in this paper is based upon work supported by the Defense Advanced Research Projects Agency (DARPA) through contract number FA8750-18-C-0089, the National Science Foundation (NSF) under grant numbers SHF 1910017 and FMitF 1918450, and the Air Force Office of Scientific Research (AFOSR) through award numbers FA9550-18-1-0122 and FA9550-19-1-0288. The U.S. Government is authorized to reproduce and distribute reprints for Government purposes notwithstanding any copyright notation thereon. Any opinions, finding, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of AFOSR, DARPA, or NSF. Publisher Copyright: {\textcopyright} 2020, The Author(s).; 32nd International Conference on Computer Aided Verification, CAV 2020 ; Conference date: 21-07-2020 Through 24-07-2020",
year = "2020",
doi = "10.1007/978-3-030-53288-8_1",
language = "English (US)",
isbn = "9783030532871",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer",
pages = "3--17",
editor = "Lahiri, {Shuvendu K.} and Chao Wang",
booktitle = "Computer Aided Verification - 32nd International Conference, CAV 2020, Proceedings",
}