Hugging Face's logo

Buckets:
huggingchat
/
papers-content

Files
xet
huggingchat/papers-content / 2004 /2004.05519.md
mishig's picture
mishig
preview code
|
download
raw
68.4 kB

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

Hoang-Dung Tran1, Xiaodong Yang1, Diego Manzanas Lopez1, Patrick Musau1, Luan Viet Nguyen2, Weiming Xiang1, Stanley Bak and Taylor T. Johnson1

1 Institute for Software Integrated Systems, Vanderbilt University, TN, USA

2 Department of Computer and Information Science, University of Pennsylvania, PA, USA

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.

1 Introduction

Deep neural networks (DNNs) have quickly become one of the most widely used tools for dealing with complex and challenging problems in numerous domains, such as image classification [10, 16, 25], function approximation, and natural language translation [11, 18]. Recently, DNNs have been used in safety-critical cyber-physical systems (CPS), such as autonomous vehicles [8, 9, 47] and air traffic collision avoidance systems [21]. Although utilizing DNNs in safety-critical applications can demonstrate considerable performance benefits, assuring the safety and robustness of these systems is challenging because DNNs possess complex non-linear characteristics. Moreover, it has been demonstrated that```

graph LR subgraph Computation_Engine [Computation Engine] direction LR CC[FFNN, CNN Constructor] RS[Reachability solvers] E[Evaluator] CC --> RS CC --> E RS --> E end subgraph Analyzer [Analyzer] direction TB V[Visualizer] SC[Safety Checker] F[Falsifier] V --> SC SC --> F end

NC[Network Configuration] --> CC
PC[Plant Configuration] --> CC
IC1[Initial Condition] --> RS
IC1 --> E
RS --> RS_out[Reachable Sets]
RS --> ET_out[Evaluation Traces]
ET_out --> E

RS_out --> V
ET_out --> F
SS[Safety Specification] --> F

V --> Plot[Plot of reachable sets/ traces]
SC --> Status[Safe/Unsafe/Uncertain]
F --> Counter[Set of counter inputs or unsafe traces]


Fig. 1: An overview of NNV and its major modules and components.

their behavior can be unpredictable due to slight perturbations in their inputs (i.e., adversarial perturbations) [35].

In this paper, we introduce the NNV (**N**eural **N**etwork **V**erification) tool, which is a software framework that performs set-based verification for DNNs and learning-enabled CPS, known colloquially as neural network control systems (NNCS) as shown in Figure 2<sup>3</sup>. NNV provides a set of reachability algorithms that can compute both the exact and over-approximate reachable sets of DNNs and NNCSs using a variety of set representations such as polyhedra [38, 48–51], star sets [28, 36, 37, 39], zonotopes [31], and abstract domain representations [32]. The reachable set obtained from NNV contains all possible states of a DNN from bounded input sets or of a NNCS from sets of initial states of a plant model. NNV declares a DNN or a NNCS to be safe if, and only if, their reachable sets do not violate safety properties (i.e., have a non-empty intersection with any state satisfying the negation of the safety property). If a safety property is violated, NNV can construct a complete set of counter-examples demonstrating the set of all possible unsafe initial inputs and states by using the star-based exact reachability algorithm [36, 39]. To speed up computation, NNV uses parallel computing, as the majority of the reachability algorithms in NNV are more efficient when executed on multi-core platforms and clusters.

NNV has been successfully applied to safety verification and robustness analysis of several real-world DNNs, primarily feedforward neural networks (FFNNs) and convolutional neural networks (CNNs), as well as learning-enabled CPS. To highlight NNV’s capabilities, we present brief experimental results from two case studies. The first compares methods for safety verification of the ACAS Xu networks [21], and the second presents safety verification of a learning-based adaptive cruise control (ACC) system.

<sup>3</sup> The source code for NNV is publicly available: <https://github.com/verivital/nnv/>. A CodeOcean capsule is also available: <https://doi.org/10.24433/CO.1314285.v1>, which will be updated with a new DOI and the latest reproducibility results if accepted. The latest version of the CodeOcean capsule with all aspects described in this paper is available at: <https://codeocean.com/capsule/1314285/>, which requires a username (taylor.johnson@uta.edu) and password (cav2020ae) to access. This account has read-only permission, so to rerun the results shown in the capsule, you can select Capsule then Duplicate from the menu bar, which will clone the capsule to allow rerunning and editing if desired. Detailed instructions for the artifact evaluation are available at: [https://github.com/verivital/run\\_nnv\\_comparison/blob/cav2020/README\\_AE.md](https://github.com/verivital/run_nnv_comparison/blob/cav2020/README_AE.md)```

graph LR
    DH[Data Hold  
u(t) = u(t_k)] -- u(t) --> P[Plant  
x-dot(t) = f(x(t), u(t))]
    P -- y(t) = Cx(t) --> S[Sampler]
    S -- v(t) --> P
    S -- v(t_k) --> FC[FFNN controller  
u(t_k) = F(y(t_k), v(t_k))]
    FC -- u(t_k) --> DH
    DH -- u(t_k) --> FC

Fig. 2: Architecture of a typical neural network control system (NNCS).
2 Overview and Features

NNV is an object-oriented toolbox written in Matlab, which was chosen in part due to the prevalence of Matlab/Simulink in the design of CPS. It uses the MPT toolbox [26] for polytope-based reachability analysis and visualization [38], and makes use of CORA [3] for zonotope-based reachability analysis of nonlinear plant models [36]. NNV also utilizes the Neural Network Model Transformation Tool (NNMT) for transforming neural network models from Keras and TensorFlow into Matlab using the Open Neural Network Exchange (ONNX) format, and the Hybrid Systems Model Transformation and Translation tool (HyST) [5] for plant configuration.

The NNV toolbox contains two main modules: a computation engine and an analyzer, shown in Figure 1. The computation engine module consists of four subcomponents: 1) the FFNN constructor, 2) the NNCS constructor, 3) the reachability solvers, and 4) the evaluator. The FFNN constructor takes a network configuration file as an input and generates a FFNN object. The NNCS constructor takes the FFNN object and the plant configuration, which describes the dynamics of a system, as inputs and then creates an NNCS object. Depending on the application, either the FFNN (or NNCS) object will be fed into a reachability solver to compute the reachable set of the FFNN (or NNCS) from a given initial set of states. Then, the obtained reachable set will be passed to the analyzer module. The analyzer module consists of three subcomponents: 1) a visualizer, 2) a safety checker, and 3) a falsifier. The visualizer can be called to plot the obtained reachable set. Given a safety specification, the safety checker can reason about the safety of the FFNN or NNCS with respect to the specification. When an exact (sound and complete) reachability solver is used, such as the star-based solver, the safety checker can return either "safe," or "unsafe" along with a set of counterexamples. When an over-approximate (sound) reachability solver is used, such as the zonotope-based scheme or the approximate star-based solvers, the safety checker can return either "safe" or "uncertain" (unknown). In this case, the falsifier automatically calls the evaluator to generate simulation traces to find a counterexample. If the falsifier can find a counterexample, then NNV returns unsafe. Otherwise, it returns unknown. A summary of NNV's major features is given in Table 1.

3 Set Representations and Reachability Algorithms

NNV implements a set of reachability algorithms for sequential FFNNs and CNNs, as well as NNCS with FFNN controllers as shown in Figure 2. The reachable set of a sequential FFNN is computed layer-by-layer. The output reachable set of a layer is the input set of the next layer in the network.

Feature Exact Analysis Over-approximate Analysis
Components FFNN, CNN, NNCS FFNN, CNN, NNCS
Plant dynamics (for NNCS) Linear ODE Linear ODE, Nonlinear ODE
Discrete/Continuous (for NNCS) Discrete Time Discrete Time, Continuous Time
Activation functions ReLU, Satlin ReLU, Satlin, Sigmoid, Tanh
CNN Layers MaxPool, Conv, BN, AvgPool, FC MaxPool, Conv, BN, AvgPool, FC MaxPool, Conv, BN, AvgPool, FC
Reachability methods Star, Polyhedron, ImageStar Star, Zonotope, Abstract-domain, ImageStar
Reachable set/Flow-pipe Visualization Yes Yes
Parallel computing Yes Partially supported
Safety verification Yes Yes
Falsification Yes Yes
Robustness verification (for FFNN/CNN) Yes Yes
Counterexample generation Yes Yes

Table 1: Overview of major features available in NNV. Links refer to relevant files/classes in the NNV codebase. BN refers to batch normalization layers, FC to fully-connected layers, AvgPool to average pooling layers, Conv to convolutional layers, and MaxPool to max pooling layers.

3.1 Polyhedron [38]

The polyhedron reachability algorithm computes the exact polyhedron reachable set of a FFNN with ReLU activation functions. The exact reachability computation of layer $L$ in a FFNN is done as follows. First, we construct the affine mapping $\bar{I}$ of the input polyhedron set $I$ , using the weight matrix $W$ and the bias vector $b$ , i.e., $\bar{I} = W \times I + b$ . Then, the exact reachable set of the layer $R_L$ is constructed by executing a sequence of stepReLU operations, i.e., $R_L = \text{stepReLU}n(\text{stepReLU}{n-1}(\dots(\text{stepReLU}_1(\bar{I}))))$ . Since a stepReLU operation can split a polyhedron into two new polyhedra, the exact reachable set of a layer in a FFNN is usually a union of polyhedra. The polyhedron reachability algorithm is computationally expensive because computing affine mappings with polyhedra is costly. Additionally, when computing the reachable set, the polyhedron approach extensively uses the expensive conversion between the H-representation and the V-representation. These are the main drawbacks that limit the scalability of the polyhedron approach. Despite that, we extend the polyhedron reachability algorithm for NNCSs with FFNN controllers. However, the propagation of polyhedra in NNCS may lead to a large degree of conservativeness in the computed reachable set [36].

3.2 Star Set [36, 39] (code)

The star set is an efficient set representation for simulation-based verification of large linear systems [6, 7, 40] where the superposition property of a linear system can be exploited in the analysis. It has been shown in [39] that the star set is also suitable for reachability analysis of FFNNs. In contrast to polyhedra, the affine mapping and intersection with a half space of a star set is more easily computed. NNV implements an enhanced version of the exact and over-approximate reachability algorithms for FFNNs proposed in [39] by minimizing the number of LP optimization problems that need to be solved in the computation. The exact algorithm that makes use of star sets is similar to the polyhedron methodthat makes use of stepReLU operations. However, it is much faster and more scalable than the polyhedron method because of the advantage that star sets have in affine mapping and intersection. The approximate algorithm obtains an over-approximation of the exact reachable set by approximating the exact reachable set after applying an activation function, e.g., ReLU, Tanh, Sigmoid. We refer readers to [39] for a detailed discussion of star-set reachability algorithms for FFNNs.

We note that NNV implements enhanced versions of earlier star-based reachability algorithms [39]. Particularly, we minimize the number of linear programming (LP) optimization problems that must be solved in order to construct the reachable set of a FFNN by quickly estimating the ranges of all of the states in the star set using only the ranges of the predicate variables. Additionally, the extensions of the star reachability algorithms to NNCS with linear plant models can eliminate the explosion of conservativeness in the polyhedron method [36,37]. The reason behind this is that in star sets, the relationship between the plant state variables and the control inputs is preserved in the computation since they are defined by a unique set of predicate variables. We refer readers to [36,37] for a detailed discussion of the extensions of the star-based reachability algorithms for NNCSs with linear/nonlinear plant models.

3.3 Zonotope [31] (code)

NNV implements the zonotope reachability algorithms proposed in [31] for FFNNs. Similar to the over-approximate algorithm using star sets, the zonotope algorithm computes an over-approximation of the exact reachable set of a FFNN. Although the zonotope reachability algorithm is very fast and scalable, it produces a very conservative reachable set in comparison to the star set method as shown in [39]. Consequently, zonotope-based reachability algorithms are usually only more efficient for very small input sets. As an example it can be more suitable for robustness certification.

3.4 Abstract Domain [32]

NNV implements the abstract domain reachability algorithm proposed in [32] for FFNNs. NNV’s abstract domain reachability algorithm specifies an abstract domain as a star set and uses a “back-tracking” approach to estimate the over-approximate ranges of the states. The abstract domain is more conservative than the star set method.

3.5 ImageStar Set (code)

NNV recently introduced a new set representation called the ImageStar for use in the verification of deep convolutional neural networks (CNNs). Briefly, the ImageStar is a generalization of the star set where the anchor and generator vectors are replaced by multi-channel images. The ImageStar is efficient in the analysis of convolutional layers, average pooling layers, and fully connected layers,whereas max pooling layers and ReLU layers consume most of computation time in reachability analysis of CNNs. NNV implements exact and over-approximate reachability algorithms using the ImageStar for serial CNNs. Since the ImageStar method has not been published yet, we defer its evaluation in our experimental evaluation. In short, using the ImageStar, we can analyze the robustness under adversarial attacks of the real-world VGG16 and VGG19 deep perception networks [30] that consist of > 100 million parameters.

4 Evaluation

The experiments presented in this section were performed on a desktop with the following configuration: Intel Core i7-6700 CPU @ 3.4GHz 8 core Processor, 64 GB Memory, and 64-bit Ubuntu 16.04.3 LTS OS.

4.1 Safety verification of ACAS Xu networks

We evaluate NNV in comparison to Reluplex [22], Marabou [23], and ReluVal [44], by considering the verification of safety property $\phi_3$ , and $\phi_4$ of the ACAS Xu neural networks [21] for all 45 networks.4 All the experiments were done using 4 cores for the computation. The verification results are summarized in Table 2 where (SAT) denotes that the networks are safe, (UNSAT) denotes unsafe, and (UNK) denotes unknown. We note that (UNK) may occur due to the conservativeness of the reachability analysis scheme. Detailed verification results are presented in the appendix. For a fast comparison with other tools, we also tested a subset input of Property 1-4 on all the 45 networks. The results are also shown in the appendix. We note that the polyhedron method [38] achieves a timeout on most of networks, and therefore, we neglect this method in the comparison.

Verification time. For property $\phi_3$ , our exact-star method is about 20.7 $\times$ faster than Reluplex, 14.2 $\times$ faster than Marabou, 81.6 $\times$ faster than Marabou-DnC (i.e., divide and conquer method). The approximate star method is 547 $\times$ faster than Reluplex, 374 $\times$ faster than Marabou, 2151 $\times$ faster than Marabou-DnC, and 8 $\times$ faster than ReluVal. For property $\phi_4$ , our exact-star method is 25.3 $\times$ faster than Reluplex, 18.0 $\times$ faster than Marabou, 53.4 $\times$ faster than Marabou-DnC, while the approximate star method is 625 $\times$ faster than Reluplex, 445 $\times$ faster than Marabou, 1321 $\times$ faster than Marabou-DnC.

Conservativeness. The approximate star method is much less conservative than the zonotope and abstract domain methods. This is illustrated since it can verify more networks than the zonotope and abstract domain methods, and is because it obtains a tighter over-approximate reachable set. For property $\phi_3$ , the zonotope and abstract domain methods can prove the safety of 2/45 networks, (4.44%) and 19/45 networks, (42.22%) respectively, while our approximate star

4 We omitted properties $\phi_1$ and $\phi_2$ for space and due to their long runtimes, but they can be reproduced in the artifact evaluation if desired.

ACAS XU \phi_3 SAT UNSAT UNK TIMEOUT TIME(s)
1h 2h 10h
Reluplex 3 42 0 2 0 0 28454
Marabou 3 42 0 1 0 0 19466
Marabou DnC 3 42 0 3 3 1 111880
ReluVal 3 42 0 0 0 0 416
Zonotope 0 2 43 0 0 0 3
Abstract Domain 0 10 35 0 0 0 72
NNV Exact Star 3 42 0 0 0 0 1371
NNV Appr. Star 0 29 16 0 0 0 52
ACAS XU \phi_4 SAT UNSAT UNK TIMEOUT TIME(s)
1h 2h 10h
Reluplex 3 42 0 0 0 0 11880
Marabou 3 42 0 0 0 0 8470
Marabou DnC 3 42 0 2 2 0 25110
ReluVal 3 42 0 0 0 0 27
Zonotope 0 1 44 0 0 0 5
Abstract Domain 0 0 45 0 0 0 7
NNV Exact Star 3 42 0 0 0 0 470
NNV Appr. Star 0 32 13 0 0 0 19

Table 2: Verification results of ACAS Xu networks.

method can prove the safety of 29/45 networks, (64.4% ). For property $\phi_4$ , the zonotope and abstract domain method can prove the safety of 1/45 networks, (2.22%) and 0/45 networks, (0.00%) respectively while the approximate star method can prove the safety of 32/45, (71.11%).

4.2 Safety Verification of Adaptive Cruise Control System

To illustrate how NNV can be used to verify/falsify safety properties of learning-enabled CPS, we analyze a learning-based ACC system depicted in Figure 3, in which the ego vehicle has a radar sensor to measure the distance to the lead vehicle in the same lane, $D_{rel}$ , as well as the relative velocity of the lead vehicle, $V_{rel}$ . The ego vehicle has two control modes. In speed control mode, it travels at a driver-specified set speed $V_{set} = 30$ , and in spacing control mode, it maintains a safe distance from the lead vehicle, $D_{safe}$ . We train a neural network with 5 layers, 20 neurons per layer utilizing the ReLU activation function to control the ego vehicle with a control period of 0.1 seconds.

We investigate safety of the learning-based ACC system with two types of plant dynamics: 1) a discrete linear plant, and 2) a nonlinear continuous plant governed by the following differential equations:

x˙lead(t)=vlead(t),v˙lead(t)=γlead,γ˙lead(t)=−2γlead(t)+2alead−μvlead2(t),x˙ego(t)=vego(t),v˙ego(t)=γego,γ˙ego(t)=−2γego(t)+2aego−μvego2(t),\begin{aligned} \dot{x}_{lead}(t) &= v_{lead}(t), \quad \dot{v}_{lead}(t) = \gamma_{lead}, \quad \dot{\gamma}_{lead}(t) = -2\gamma_{lead}(t) + 2a_{lead} - \mu v_{lead}^2(t), \\ \dot{x}_{ego}(t) &= v_{ego}(t), \quad \dot{v}_{ego}(t) = \gamma_{ego}, \quad \dot{\gamma}_{ego}(t) = -2\gamma_{ego}(t) + 2a_{ego} - \mu v_{ego}^2(t), \end{aligned}

where $x_{lead}(x_{ego})$ , $v_{lead}(v_{ego})$ and $\gamma_{lead}(\gamma_{ego})$ are the position, velocity and acceleration of the lead (ego) vehicle respectively. $a_{lead}(a_{ego})$ is the acceleration control input applied to the lead (ego) vehicle, and $\mu = 0.0001$ is a friction parameter. To obtain a discrete linear model of the plant, we let $\mu = 0$ andFig. 3: Learning-based Adaptive Cruise Control System [1].

discretize the corresponding linear continuous model using a zero-order hold on the inputs with a sample time of 0.1 seconds (i.e., the control period).

Verification Problem. The scenario we are interested in is when the two vehicles are operating at a safe distance between them and the ego vehicle is in speed control mode. In this state the lead vehicle driver suddenly decelerates with $a_{lead} = -5$ to reduce the speed. We want to verify if the neural network controller on the ego vehicle will also de-accelerate to maintain a safe distance between the two vehicles. To guarantee safety, we require that $D_{rel} = x_{lead} - x_{ego} \geq D_{safe} = D_{default} + T_{gap} \times v_{ego}$ where $T_{gap} = 1.4$ seconds and $D_{default} = 10$ . Our analysis investigates if the safety requirement holds in the 5 seconds after the lead vehicle decelerates. We consider the safety of the system under the following initial conditions: $x_{lead}(0) \in [90, 92]$ , $v_{lead}(0) \in [20, 30]$ , $\gamma_{lead}(0) = \gamma_{ego}(0) = 0$ , $v_{ego}(0) \in [30, 30.5]$ , $x_{ego} \in [30, 31]$ .

Verification results. For linear dynamics, NNV can compute both the exact and over-approximate reachable sets of the ACC system in bounded time steps, while for nonlinear dynamics, NNV constructs an over-approximation of the exact reachable sets and uses it for safety verification. The verification results for linear and nonlinear models using the over-approximate star method are presented in Table 3, which shows that, the safety of the ACC system depends on the initial velocity of the lead vehicle. When the initial velocity of the lead vehicle is smaller than $27(m/s)$ , the ACC system with the discrete plant model is unsafe. Using the exact star method, NNV can construct a complete set of counter-example inputs. When the over-approximate star method is used, if there is a potential safety violation, NNV simulates the system with 1000 random inputs from the input set to find counter examples. If a counterexample is found, the system is UNSAFE, otherwise, NNV returns a safety result of UNKNOWN. Figure 4 visualizes the reachable sets of the relative distance $D_{rel}$ between two vehicles versus the required safe distance $D_{safe}$ over time for two cases of initial velocities of the lead vehicle: $v_{lead}(0) \in [29, 30]$ and $v_{lead}(0) \in [24, 25]$ . We can see that in the first case, $D_{ref} \geq D_{safe}$ for all 50 time steps stating that the system is safe. In the second case, $D_{ref} < D_{safe}$ in some control steps which means that the system is unsafe. NNV supports a reachLive method to perform analysis and reachable set visualization on-the-fly to help the user observe the behavior of the system during verification.

The verification results for ACC system with the nonlinear model are all UNSAFE, which is surprising. Since the neural network controller of the ACC system was trained with the linear model, it works quite well for the linear model. However, when a small friction term is added to the linear model to form a

v_{lead}(0) Linear Plant Nonlinear Plant
Safety VT(s) Safety VT(s)
[29, 30] SAFE 9.60 UNSAFE 346.62
[28, 29] SAFE 9.45 UNSAFE 277.50
[27, 28] SAFE 9.82 UNSAFE 289.70
[26, 27] UNSAFE 17.80 UNSAFE 315.60
[25, 26] UNSAFE 19.24 UNSAFE 305.56
[24, 25] UNSAFE 18.12 UNSAFE 372.00

Table 3: Verification results for ACC system with different plant models, where $VT$ is the verification time (in seconds).

Fig. 4: Two scenarios of the ACC system. In the first (top) scenario ( $v_{lead}(0) \in [29, 30]m/s$ ), safety is guaranteed, $D_{rel} \geq D_{safe}$ . In the second scenario (bottom) ( $v_{lead}(0) \in [24, 25]m/s$ ), safety is violated since $D_{ref} < D_{safe}$ in some control steps.

nonlinear model, the neural network controller’s performance, in terms of safety, is significantly reduced. This problem raises an important issue in training neural network controllers using simulation data, and these schemes may not work in real systems since there is always a mismatch between the plant model in the simulation engine and the real system.

Verification times. As shown in Table 3, the approximate analysis of the ACC system with discrete linear plant model is very fast. It can be done in 84 seconds. We note that NNV also supports exact analysis, which is computationally expensive since it constructs all reachable sets of the system. Because there are splits in the reachable sets of the neural network controller, the number of star sets in the reachable set of the plant increases quickly over time [36]. In contrast, the over-approximate method computes the interval hull of all reachable star sets at each time step. It maintains a single reachable set of the plant throughout the computation. Therefore, the over-approximate method is muchfaster than the exact method. In terms of plant models, the nonlinear model requires more computation time than the linear one. As shown in Table 3, the verification for linear model using the over-approximate method is $22.7\times$ faster on average than the verification of the nonlinear model.

5 Related Work

NNV was inspired by many insightful research works in the emerging fields of neural network and machine learning verification. For the “open-loop” verification problem (verification of DNNs), many efficient techniques have been proposed, such as SMT-based methods [22, 23, 29], mixed-integer linear programming methods [14, 24, 27], set-based methods [4, 17, 31, 32, 43, 45, 49], and optimization methods [46, 52]. For the “closed-loop” verification problem (NNCS verification), we note that the Verisig approach [20] is very efficient for NNCS with nonlinear plants and with Sigmoid and Tanh activation functions. Additionally, the recent regressive polynomial rule inference approach [33] is very fast for the safety verification of NNCS with nonlinear plant models and ReLU activation functions. The satisfiability modulo convex (SMC) approach [34] is also very promising for NNCS with discrete linear plants as it provides both soundness and completeness properties in verification. ReachNN [19] is a recent approach that can efficiently control the conservativeness in the reachability analysis of NNCS with nonlinear plants and ReLU, Sigmoid and Tanh activation functions in the controller. In other learning-enabled systems, falsification and testing-based approaches [12, 13, 41] have shown a significant promise in enhancing the safety of systems where perception components and neural network controllers interact with the physical world. Finally, there is significant related work in the domain of safe reinforcement learning [2, 15, 42, 53] and combining guarantees from NNV with those provided in these methods would be interesting to explore.

6 Conclusion and Future Work

We have presented NNV, a toolbox for the verification of DNNs and learning-enabled CPS. Our tool provides a collection of reachability algorithms that can be used to verify the safety (and robustness) of real-world DNNs as well as learning-enabled CPS, such as the ACC system. Our method is comparable to existing methods such as Reluplex and Marabou when dealing with the open-loop verification problem. For closed-loop systems, NNV can compute the exact and over-approximate reachable sets of a NNCS with linear plant models. For a NNCS with a nonlinear plant, NNV can obtain an over-approximate reachable set and use it to verify the safety, but can also automatically falsify the system to construct/find counterexamples (using exact analysis) or randomized simulations (in over-approximate analysis).## References

    1. 2019b, M.: Model Predictive Control Toolbox. The MathWorks Inc., Natick, Massachusetts (2019), https://www.mathworks.com/help/mpc/ug/adaptive-cruise-control-using-model-predictive-controller.html
    1. Alshiekh, M., Bloem, R., Ehlers, R., Könighofer, B., Niekum, S., Topcu, U.: Safe reinforcement learning via shielding. In: Thirty-Second AAAI Conference on Artificial Intelligence (2018)
    1. Althoff, M.: An introduction to cora 2015. In: Proc. of the Workshop on Applied Verification for Continuous and Hybrid Systems (2015)
    1. Anderson, G., Pailoor, S., Dillig, I., Chaudhuri, S.: Optimization and abstraction: A synergistic approach for analyzing neural network robustness. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. p. 731744. PLDI 2019, Association for Computing Machinery, New York, NY, USA (2019), https://doi.org/10.1145/3314221.3314614
    1. Bak, S., Bogomolov, S., Johnson, T.T.: Hyst: a source transformation and translation tool for hybrid automaton models. In: Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control. pp. 128–133. ACM (2015)
    1. Bak, S., Duggirala, P.S.: Simulation-equivalent reachability of large linear systems with inputs. In: International Conference on Computer Aided Verification. pp. 401–420. Springer (2017)
    1. Bak, S., Tran, H.D., Johnson, T.T.: Numerical verification of affine systems with up to a billion dimensions. In: Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control. pp. 23–32. ACM (2019)
    1. Bojarski, M., Del Testa, D., Dworakowski, D., Firner, B., Flepp, B., Goyal, P., Jackel, L.D., Monfort, M., Muller, U., Zhang, J., et al.: End to end learning for self-driving cars. arXiv preprint arXiv:1604.07316 (2016)
    1. Chen, C., Seff, A., Kornhauser, A., Xiao, J.: Deepdriving: Learning affordance for direct perception in autonomous driving. In: Proceedings of the IEEE International Conference on Computer Vision. pp. 2722–2730 (2015)
    1. Cireşan, D., Meier, U., Schmidhuber, J.: Multi-column deep neural networks for image classification. arXiv preprint arXiv:1202.2745 (2012)
    1. Collobert, R., Weston, J.: A unified architecture for natural language processing: Deep neural networks with multitask learning. In: Proceedings of the 25th international conference on Machine learning. pp. 160–167. ACM (2008)
    1. Dreossi, T., Donzé, A., Seshia, S.A.: Compositional falsification of cyber-physical systems with machine learning components. In: NASA Formal Methods Symposium. pp. 357–372. Springer (2017)
    1. Dreossi, T., Fremont, D.J., Ghosh, S., Kim, E., Ravanbakhsh, H., Vazquez-Chanlatte, M., Seshia, S.A.: Verifai: A toolkit for the formal design and analysis of artificial intelligence-based systems. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification. pp. 432–442. Springer International Publishing, Cham (2019)
    1. Dutta, S., Jha, S., Sanakaranarayanan, S., Tiwari, A.: Output range analysis for deep neural networks. arXiv preprint arXiv:1709.09130 (2017)
    1. Fulton, N., Platzer, A.: Verifiably safe off-model reinforcement learning. In: Vojnar, T., Zhang, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems. pp. 413–430. Springer International Publishing, Cham (2019)
    1. Gatys, L.A., Ecker, A.S., Bethge, M.: Image style transfer using convolutional neural networks. In: Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition. pp. 2414–2423 (2016)1. 17. Gehr, T., Mirman, M., Drachler-Cohen, D., Tsankov, P., Chaudhuri, S., Vechev, M.: Ai 2: Safety and robustness certification of neural networks with abstract interpretation. In: Security and Privacy (SP), 2018 IEEE Symposium on (2018)
    1. Goldberg, Y.: A primer on neural network models for natural language processing. Journal of Artificial Intelligence Research 57, 345–420 (2016)
    1. Huang, C., Fan, J., Li, W., Chen, X., Zhu, Q.: Reachnn: Reachability analysis of neural-network controlled systems. arXiv preprint arXiv:1906.10654 (2019)
    1. Ivanov, R., Weimer, J., Alur, R., Pappas, G.J., Lee, I.: Verisig: verifying safety properties of hybrid systems with neural network controllers. In: Hybrid Systems: Computation and Control (HSCC) (2019)
    1. Julian, K.D., Lopez, J., Brush, J.S., Owen, M.P., Kochenderfer, M.J.: Policy compression for aircraft collision avoidance systems. In: Digital Avionics Systems Conference (DASC), 2016 IEEE/AIAA 35th. pp. 1–10. IEEE (2016)
    1. Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: An efficient smt solver for verifying deep neural networks. In: International Conference on Computer Aided Verification. pp. 97–117. Springer (2017)
    1. Katz, G., Huang, D.A., Ibeling, D., Julian, K., Lazarus, C., Lim, R., Shah, P., Thakoor, S., Wu, H., Zeljić, A., et al.: The marabou framework for verification and analysis of deep neural networks. In: International Conference on Computer Aided Verification. pp. 443–452. Springer (2019)
    1. Kouvaros, P., Lomuscio, A.: Formal verification of cnn-based perception systems. arXiv preprint arXiv:1811.11373 (2018)
    1. Krizhevsky, A., Sutskever, I., Hinton, G.E.: Imagenet classification with deep convolutional neural networks. In: Advances in neural information processing systems. pp. 1097–1105 (2012)
    1. Kvasnica, M., Grieder, P., Baotic, M., Morari, M.: Multi-parametric toolbox (mpt). In: International Workshop on Hybrid Systems: Computation and Control. pp. 448–462. Springer (2004)
    1. Lomuscio, A., Maganti, L.: An approach to reachability analysis for feed-forward relu neural networks. arXiv preprint arXiv:1706.07351 (2017)
    1. Lopez, D.M., Musau, P., Tran, H.D., Johnson, T.T.: Verification of closed-loop systems with neural network controllers. In: Frehse, G., Althoff, M. (eds.) ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systems. EPiC Series in Computing, vol. 61, pp. 201–210. EasyChair (April 2019), https://easychair.org/publications/paper/ZmnC
    1. Pulina, L., Tacchella, A.: An abstraction-refinement approach to verification of artificial neural networks. In: International Conference on Computer Aided Verification. pp. 243–257. Springer (2010)
    1. Simonyan, K., Zisserman, A.: Very deep convolutional networks for large-scale image recognition. arXiv preprint arXiv:1409.1556 (2014)
    1. Singh, G., Gehr, T., Mirman, M., Püschel, M., Vechev, M.: Fast and effective robustness certification. In: Advances in Neural Information Processing Systems. pp. 10825–10836 (2018)
    1. Singh, G., Gehr, T., Püschel, M., Vechev, M.: An abstract domain for certifying neural networks. Proceedings of the ACM on Programming Languages 3(POPL), 41 (2019)
    1. Souradeep Dutta, Xin Chen, S.S.: Reachability analysis for neural feedback systems using regressive polynomial rule inference. In: Hybrid Systems: Computation and Control (HSCC) (2019)1. 34. Sun, X., Khedr, H., Shoukry, Y.: Formal verification of neural network controlled autonomous systems. In: Hybrid Systems: Computation and Control (HSCC) (2019)
    1. Szegedy, C., Zaremba, W., Sutskever, I., Bruna, J., Erhan, D., Goodfellow, I., Fergus, R.: Intriguing properties of neural networks. arXiv preprint arXiv:1312.6199 (2013)
    1. Tran, H.D., Ce, F., Lopez, D.M., Johnson, T.T., Koutsoukos, X.: Safety verification of cyber-physical systems with reinforcement learning control. In: ACM SIGBED International Conference on Embedded Software (EMSOFT'19). ACM (October 2019)
    1. Tran, H.D., Ce, F., Lopez, D.M., Johnson, T.T., Koutsoukos, X.: Safety verification of cyber-physical systems with reinforcement learning control (July 2019)
    1. Tran, H.D., Musau, P., Lopez, D.M., Yang, X., Nguyen, L.V., Xiang, W., Johnson, T.T.: Parallelizable reachability analysis algorithms for feed-forward neural networks. In: 7th International Conference on Formal Methods in Software Engineering (FormaliSE2019), Montreal, Canada (2019)
    1. Tran, H.D., Musau, P., Lopez, D.M., Yang, X., Nguyen, L.V., Xiang, W., Johnson, T.T.: Star-based reachability analysis for deep neural networks. In: 23rd International Symposium on Formal Methods (FM'19). Springer International Publishing (October 2019)
    1. Tran, H.D., Nguyen, L.V., Hamilton, N., Xiang, W., Johnson, T.T.: Reachability analysis for high-index linear differential algebraic equations (daes). In: 17th International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'19). Springer International Publishing (August 2019)
    1. Tuncali, C.E., Fainekos, G., Ito, H., Kapinski, J.: Simulation-based adversarial test generation for autonomous vehicles with machine learning components. arXiv preprint arXiv:1804.06760 (2018)
    1. Verma, A., Murali, V., Singh, R., Kohli, P., Chaudhuri, S.: Programmatically interpretable reinforcement learning. In: Dy, J., Krause, A. (eds.) Proceedings of the 35th International Conference on Machine Learning. Proceedings of Machine Learning Research, vol. 80, pp. 5045–5054. PMLR, Stockholmsmssan, Stockholm Sweden (10–15 Jul 2018), http://proceedings.mlr.press/v80/verma18a.html
    1. Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Efficient formal safety analysis of neural networks. In: Advances in Neural Information Processing Systems. pp. 6369–6379 (2018)
    1. Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Formal security analysis of neural networks using symbolic intervals. In: 27th USENIX Security Symposium (USENIX Security 18). USENIX Association, Baltimore, MD (2018), https://www.usenix.org/conference/usenixsecurity18/presentation/wang-shiqi
    1. Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Formal security analysis of neural networks using symbolic intervals. arXiv preprint arXiv:1804.10829 (2018)
    1. Weng, T.W., Zhang, H., Chen, H., Song, Z., Hsieh, C.J., Boning, D., Dhillon, I.S., Daniel, L.: Towards fast computation of certified robustness for relu networks. arXiv preprint arXiv:1804.09699 (2018)
    1. Wu, B., Iandola, F.N., Jin, P.H., Keutzer, K.: Squeezedet: Unified, small, low power fully convolutional neural networks for real-time object detection for autonomous driving. In: CVPR Workshops. pp. 446–454 (2017)
    1. Xiang, W., Tran, H.D., Johnson, T.T.: Reachable set computation and safety verification for neural networks with relu activations. arXiv preprint arXiv:1712.08163 (2017)1. 49. Xiang, W., Tran, H.D., Johnson, T.T.: Output reachable set estimation and verification for multilayer neural networks. IEEE transactions on neural networks and learning systems (99), 1–7 (2018)
    1. Xiang, W., Tran, H.D., Johnson, T.T.: Specification-guided safety verification for feedforward neural networks. AAAI Spring Symposium on Verification of Neural Networks (2019)
    1. Xiang, W., Tran, H.D., Rosenfeld, J.A., Johnson, T.T.: Reachable set estimation and safety verification for piecewise linear systems with neural network controllers. arXiv preprint arXiv:1802.06981 (2018)
    1. Zhang, H., Weng, T.W., Chen, P.Y., Hsieh, C.J., Daniel, L.: Efficient neural network robustness certification with general activation functions. In: Advances in Neural Information Processing Systems. pp. 4944–4953 (2018)
    1. Zhu, H., Xiong, Z., Magill, S., Jagannathan, S.: An inductive synthesis framework for verifiable reinforcement learning. In: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. p. 686701. PLDI 2019, Association for Computing Machinery, New York, NY, USA (2019), https://doi.org/10.1145/3314221.3314638## A Appendix: Additional Evaluation Details

Figures 5 and 6 show detailed comparisons between NNV’s approximate and exact star methods relative to the zonotope, abstract domain, Reluplex, Marabou, and Marabou divide-and-conquer (DnC) methods, summarized earlier in Table 2.

ID Zonotope Abstract Domain Reluplex Marabou Marabou DnC ReluVal NNV Exact Star NNV Appr. Star
VT V VT V VT V VT V VT V VT V N_p VT V VT V
N_{11}0.05UNK1.96UNSAT6156UNSAT3637UNSAT73560UNSAT96.83UNSAT70631398.50UNSAT1.89UNK
N_{12}0.06UNK2.31UNSAT4942UNSAT3418UNSAT3221UNSAT1.87UNSAT39529205.88UNSAT1.86UNK
N_{13}0.07UNK2.42UNSAT1134UNSAT1795UNSAT10858UNSAT3.22UNSAT1227445.62UNSAT2.16UNK
N_{14}0.06UNK1.73UNK528UNSAT187UNSAT186UNSAT0.27UNSAT427512.29UNSAT1.04UNSAT
N_{15}0.07UNK1.68UNK317UNSAT124UNSAT193UNSAT0.11UNSAT474416.45UNSAT0.96UNSAT
N_{16}0.06UNK0.99UNSAT64UNSAT37UNSAT23UNSAT0.04UNSAT12665.70UNSAT0.79UNSAT
N_{17}0.07UNK0.73UNK1SAT5SAT6SAT0.03SAT5002.76SAT0.64UNK
N_{18}0.05UNK0.62UNK3SAT2SAT6SAT0.03SAT3932.39SAT0.45UNK
N_{19}0.06UNK0.52UNK2SAT2SAT6SAT0.03SAT2902.18SAT0.42UNK
N_{21}0.06UNK2.36UNK1208UNSAT1001UNSAT813UNSAT18.46UNSAT1617954.05UNSAT1.79UNK
N_{22}0.06UNK1.64UNK653UNSAT480UNSAT2106UNSAT7.22UNSAT686120.62UNSAT1.39UNK
N_{23}0.06UNK1.93UNK1043UNSAT1103UNSAT1163UNSAT2.73UNSAT1061432.19UNSAT1.69UNK
N_{24}0.05UNK1.01UNSAT41UNSAT22UNSAT8UNSAT0.48UNSAT3452.43UNSAT0.55UNSAT
N_{25}0.06UNK1.82UNK235UNSAT58UNSAT13UNSAT0.31UNSAT24568.38UNSAT1.17UNSAT
N_{26}0.07UNK0.82UNSAT79UNSAT23UNSAT8UNSAT0.03UNSAT2532.45UNSAT0.69UNSAT
N_{27}0.06UNK1.53UNSAT116UNSAT57UNSAT9UNSAT0.20UNSAT11995.29UNSAT1.01UNSAT
N_{28}0.06UNK1.03UNSAT83UNSAT13UNSAT8UNSAT0.04UNSAT3262.58UNSAT0.50UNSAT
N_{29}0.05UNSAT0.38UNSAT27UNSAT2UNSAT7UNSAT0.01UNSAT1882.13UNSAT0.36UNSAT
N_{31}0.06UNK2.41UNSAT177UNSAT97UNSAT240UNSAT2.58UNSAT596719.97UNSAT1.13UNSAT
N_{32}0.07UNK2.32UNK1561UNSAT1973UNSAT1564UNSAT5.27UNSAT36967183.86UNSAT1.91UNK
N_{33}0.08UNK2.09UNSAT1105UNSAT344UNSAT891UNSAT0.26UNSAT784830.29UNSAT1.76UNSAT
N_{34}0.06UNK2.89UNK209UNSAT106UNSAT34UNSAT0.49UNSAT20779.35UNSAT1.96UNK
N_{35}0.06UNK1.50UNK83UNSAT41UNSAT10UNSAT5.01UNSAT10345.08UNSAT1.16UNSAT
N_{36}0.07UNK2.50UNK255UNSAT120UNSAT194UNSAT138.73UNSAT18578.04UNSAT1.86UNK
N_{37}0.05UNK0.76UNSAT35UNSAT8UNSAT7UNSAT0.10UNSAT1071.95UNSAT0.56UNSAT
N_{38}0.07UNK1.34UNK179UNSAT57UNSAT25UNSAT3.51UNSAT6543.66UNSAT1.04UNSAT
N_{39}0.08UNK1.54UNK118UNSAT55UNSAT35UNSAT2.36UNSAT12015.50UNSAT0.75UNSAT
N_{41}0.07UNK1.34UNK201UNSAT94UNSAT914UNSAT7.29UNSAT22768.68UNSAT1.20UNK
N_{42}0.05UNK2.13UNK2882UNSAT1724UNSAT11861UNSAT90.93UNSAT1789468.22UNSAT1.67UNK
N_{43}0.07UNK2.05UNK1767UNSAT1257UNSAT1014UNSAT2.13UNSAT2074698.76UNSAT1.79UNK
N_{44}0.07UNK1.51UNK86UNSAT19UNSAT8UNSAT0.11UNSAT5603.38UNSAT0.94UNSAT
N_{45}0.06UNK0.90UNSAT35UNSAT14UNSAT8UNSAT0.09UNSAT3512.34UNSAT0.77UNSAT
N_{46}0.05UNK2.78UNSAT300UNSAT118UNSAT55UNSAT0.14UNSAT249611.33UNSAT2.60UNSAT
N_{47}0.06UNK1.45UNK126UNSAT54UNSAT43UNSAT0.52UNSAT9444.68UNSAT0.70UNSAT
N_{48}0.07UNK1.33UNSAT142UNSAT36UNSAT41UNSAT1.65UNSAT5763.46UNSAT0.81UNSAT
N_{49}0.06UNK2.41UNSAT143UNSAT33UNSAT22UNSAT0.07UNSAT6115.07UNSAT1.02UNSAT
N_{51}0.06UNK1.65UNK1131UNSAT764UNSAT1910UNSAT19.33UNSAT946129.50UNSAT1.47UNK
N_{52}0.05UNK1.15UNK151UNSAT120UNSAT635UNSAT1.94UNSAT21048.17UNSAT1.01UNSAT
N_{53}0.17UNK1.73UNSAT341UNSAT146UNSAT64UNSAT0.13UNSAT28749.08UNSAT1.41UNSAT
N_{54}0.06UNK1.53UNK62UNSAT42UNSAT10UNSAT0.13UNSAT7584.50UNSAT1.06UNSAT
N_{55}0.07UNK1.83UNK86UNSAT27UNSAT18UNSAT0.41UNSAT13055.59UNSAT1.06UNSAT
N_{56}0.07UNK2.14UNK283UNSAT81UNSAT47UNSAT0.86UNSAT11435.73UNSAT1.12UNSAT
N_{57}0.07UNSAT0.43UNSAT35UNSAT5UNSAT8UNSAT0.02UNSAT881.81UNSAT0.34UNSAT
N_{58}0.05UNK1.58UNSAT310UNSAT157UNSAT22UNSAT0.06UNSAT23689.10UNSAT0.92UNSAT
N_{59}0.06UNK0.72UNK19UNSAT8UNSAT8UNSAT0.07UNSAT1072.03UNSAT0.58UNSAT

Fig. 5: Detailed verification results for $\phi_3$ of ACAS Xu networks.

ID Zonotope Abstract Reluplex Marabou Marabou DnC ReluVal NNV Exact Star NNV Appr. Star
VT V VT V VT V VT V VT V VT V N_p VT V VT V
N_{11}0.11UNK0.15UNK1291UNSAT1929UNSAT11379UNSAT1.08UNSAT1914363.78UNSAT0.52UNK
N_{12}0.10UNK0.15UNK1267UNSAT2012UNSAT8629UNSAT1.13UNSAT1314340.60UNSAT0.64UNK
N_{13}0.11UNK0.16UNK1150UNSAT956UNSAT2806UNSAT0.34UNSAT983731.32UNSAT0.71UNK
N_{14}0.10UNK0.16UNK107UNSAT79UNSAT93UNSAT0.18UNSAT11844.86UNSAT0.30UNK
N_{15}0.11UNK1.15UNK352UNSAT299UNSAT267UNSAT0.41UNSAT660822.23UNSAT0.33UNK
N_{16}0.11UNK0.15UNK219UNSAT201UNSAT82UNSAT0.18UNSAT444313.19UNSAT0.41UNSAT
N_{17}0.14UNK0.15UNK1SAT2SAT6SAT0.02SAT6423.21SAT0.18UNK
N_{18}0.11UNK0.15UNK3SAT2SAT6SAT0.02SAT3972.64SAT0.20UNK
N_{19}0.11UNK0.13UNK3SAT1SAT6SAT0.02SAT4712.68SAT0.16UNK
N_{21}0.11UNK0.17UNK330UNSAT239UNSAT112UNSAT1.01UNSAT506614.80UNSAT0.51UNK
N_{22}0.11UNK0.15UNK415UNSAT273UNSAT210UNSAT1.85UNSAT450014.40UNSAT0.57UNK
N_{23}0.11UNK0.15UNK243UNSAT47UNSAT35UNSAT0.93UNSAT10874.58UNSAT0.27UNSAT
N_{24}0.11UNK0.14UNK86UNSAT23UNSAT16UNSAT0.12UNSAT9134.65UNSAT0.37UNSAT
N_{25}0.11UNK0.16UNK151UNSAT95UNSAT46UNSAT0.31UNSAT341911.43UNSAT0.52UNSAT
N_{26}0.11UNK0.15UNK118UNSAT71UNSAT70UNSAT0.26UNSAT14626.33UNSAT0.60UNSAT
N_{27}0.10UNK0.16UNK34UNSAT25UNSAT8UNSAT0.04UNSAT5553.38UNSAT0.31UNSAT
N_{28}0.11UNK0.17UNK549UNSAT121UNSAT33UNSAT0.06UNSAT18058.85UNSAT1.15UNK
N_{29}0.11UNK0.13UNK52UNSAT6UNSAT7UNSAT0.02UNSAT1572.30UNSAT0.15UNSAT
N_{31}0.12UNK0.15UNK478UNSAT220UNSAT283UNSAT1.12UNSAT428113.82UNSAT0.52UNSAT
N_{32}0.13UNK0.16UNK107UNSAT237UNSAT102UNSAT0.44UNSAT870823.53UNSAT0.34UNSAT
N_{33}0.11UNK0.14UNK116UNSAT36UNSAT12UNSAT0.06UNSAT12015.13UNSAT0.26UNSAT
N_{34}0.11UNK0.14UNK75UNSAT32UNSAT13UNSAT0.15UNSAT12145.34UNSAT0.27UNSAT
N_{35}0.11UNK0.15UNK206UNSAT212UNSAT52UNSAT0.91UNSAT363015.78UNSAT0.80UNSAT
N_{36}0.14UNK0.17UNK141UNSAT50UNSAT47UNSAT1.42UNSAT14956.52UNSAT0.68UNSAT
N_{37}0.11UNK0.16UNK304UNSAT49UNSAT10UNSAT0.22UNSAT8625.18UNSAT0.25UNSAT
N_{38}0.11UNK0.15UNK131UNSAT48UNSAT20UNSAT0.23UNSAT5424.31UNSAT0.43UNK
N_{39}0.11UNK0.17UNK621UNSAT144UNSAT57UNSAT1.36UNSAT268411.72UNSAT0.56UNSAT
N_{41}0.11UNSAT0.13UNK49UNSAT30UNSAT40UNSAT2.73UNSAT8483.74UNSAT0.19UNSAT
N_{42}0.11UNK0.16UNK244UNSAT77UNSAT42UNSAT1.96UNSAT13486.16UNSAT0.45UNSAT
N_{43}0.11UNK0.15UNK243UNSAT163UNSAT100UNSAT1.10UNSAT372510.62UNSAT0.50UNSAT
N_{44}0.11UNK0.15UNK206UNSAT52UNSAT31UNSAT1.31UNSAT12536.04UNSAT0.72UNK
N_{45}0.14UNK0.16UNK217UNSAT53UNSAT32UNSAT1.49UNSAT12555.30UNSAT0.44UNSAT
N_{46}0.11UNK0.15UNK177UNSAT18UNSAT8UNSAT0.02UNSAT23668.64UNSAT0.57UNSAT
N_{47}0.13UNK0.15UNK47UNSAT16UNSAT10UNSAT0.17UNSAT2162.43UNSAT0.29UNSAT
N_{48}0.11UNK0.17UNK195UNSAT68UNSAT25UNSAT0.18UNSAT15916.87UNSAT0.47UNSAT
N_{49}0.11UNK0.17UNK422UNSAT51UNSAT19UNSAT0.08UNSAT25669.05UNSAT0.43UNSAT
N_{51}0.11UNK0.15UNK513UNSAT174UNSAT193UNSAT2.52UNSAT693217.71UNSAT0.40UNSAT
N_{52}0.11UNK0.15UNK210UNSAT48UNSAT31UNSAT0.86UNSAT436112.81UNSAT0.30UNSAT
N_{53}0.11UNK0.15UNK124UNSAT39UNSAT41UNSAT0.09UNSAT16626.54UNSAT0.43UNSAT
N_{54}0.11UNK0.15UNK144UNSAT43UNSAT12UNSAT0.12UNSAT10885.18UNSAT0.36UNSAT
N_{55}0.14UNK0.15UNK114UNSAT61UNSAT30UNSAT0.48UNSAT15496.27UNSAT0.30UNSAT
N_{56}0.10UNK0.15UNK160UNSAT55UNSAT45UNSAT0.33UNSAT6774.56UNSAT0.33UNSAT
N_{57}0.11UNK0.18UNK38UNSAT8UNSAT8UNSAT0.03UNSAT1572.12UNSAT0.24UNSAT
N_{58}0.11UNK0.16UNK111UNSAT48UNSAT22UNSAT0.06UNSAT5024.20UNSAT0.59UNSAT
N_{59}0.11UNK0.15UNK116UNSAT57UNSAT14UNSAT0.09UNSAT9925.20UNSAT0.35UNSAT

Fig. 6: Detailed verification results for $\phi_4$ of ACAS Xu networks.

Xet Storage Details

Size:
68.4 kB
·
Xet hash:
e69c9daaff9829b48a3fbc69e4bc7a5d39e4518fae550c19621b3a91562439f0

Xet efficiently stores files, intelligently splitting them into unique chunks and accelerating uploads and downloads. More info.