70 citations · 193 across the 16 of their papers we have counts for
17 papers
Deterministic World Models for Closed-loop Reachability Analysis of End-to-End Vision-based Control
Yuang Geng, Zhongzheng Zhang, Chengzhen Jiang +5
End-to-end image controllers that map raw camera frames directly to control actions are increasingly deployed in safety-critical systems. However, formally verifying their closed-l…
A Transition System Abstraction Framework for Neural Network Dynamical System Models
Yejiang Yang, Zihao Mo, Hoang-Dung Tran +1
This paper proposes a transition system abstraction framework for neural network dynamical system models to enhance the model interpretability, with applications to complex dynamic…
Neural Network Compression of ACAS Xu Early Prototype is Unsafe: Closed-Loop Verification through Quantized State Backreachability
Stanley Bak, Hoang-Dung Tran
ACAS Xu is an air-to-air collision avoidance system designed for unmanned aircraft that issues horizontal turn advisories to avoid an intruder aircraft. Due the use of a large look…
Neural Network Repair with Reachability Analysis
Xiaodong Yang, Tom Yamaguchi, Hoang-Dung Tran +3
Safety is a critical concern for the next generation of autonomy that is likely to rely heavily on deep neural networks for perception and control. Formally verifying the safety an…
Reachability Analysis of Convolutional Neural Networks
Xiaodong Yang, Tomoya Yamaguchi, Hoang-Dung Tran +3
Deep convolutional neural networks have been widely employed as an effective technique to handle complex and practical problems. However, one of the fundamental problems is the lac…
Verification of Deep Convolutional Neural Networks Using ImageStars
Hoang-Dung Tran, Stanley Bak, Weiming Xiang +1
Convolutional Neural Networks (CNN) have redefined the state-of-the-art in many real-world applications, such as facial recognition, image classification, human pose estimation, an…
Reachable Set Estimation for Neural Network Control Systems: A Simulation-Guided Approach
Weiming Xiang, Hoang-Dung Tran, Xiaodong Yang +1
The vulnerability of artificial intelligence (AI) and machine learning (ML) against adversarial disturbances and attacks significantly restricts their applicability in safety-criti…
NNV: The Neural Network Verification Tool for Deep Neural Networks and Learning-Enabled Cyber-Physical Systems
Hoang-Dung Tran, Xiaodong Yang, Diego Manzanas Lopez +5
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 syst…
Reachability Analysis for Feed-Forward Neural Networks using Face Lattices
Xiaodong Yang, Hoang-Dung Tran, Weiming Xiang +1
The paper introduces a parallelizable method that uses face lattices to compute exact reachable sets for feed‑forward ReLU neural networks, enabling more efficient safety verificat…
Real-Time Verification for Distributed Cyber-Physical Systems
Hoang-Dung Tran, Luan Viet Nguyen, Patrick Musau +2
Safety-critical distributed cyber-physical systems (CPSs) have been found in a wide range of applications. Notably, they have displayed a great deal of utility in intelligent trans…
Specification-Guided Safety Verification for Feedforward Neural Networks
Weiming Xiang, Hoang-Dung Tran, Taylor T. Johnson
This paper presents a specification-guided safety verification method for feedforward neural networks with general activation functions. As such feedforward networks are memoryless…
Simulation-Based Reachability Analysis for High-Index Large Linear Differential Algebraic Equations
Hoang-Dung Tran, Weiming Xiang, Nathaniel Hamilton +1
Reachability analysis is a fundamental problem for safety verification and falsification of Cyber-Physical Systems (CPS) whose dynamics follow physical laws usually represented as…
Numerical Verification of Affine Systems with up to a Billion Dimensions
Stanley Bak, Hoang-Dung Tran, Taylor T. Johnson
Affine systems reachability is the basis of many verification methods. With further computation, methods exist to reason about richer models with inputs, nonlinear differential equ…
Reachable Set Estimation and Safety Verification for Piecewise Linear Systems with Neural Network Controllers
Weiming Xiang, Hoang-Dung Tran, Joel A. Rosenfeld +1
In this work, the reachable set estimation and safety verification problems for a class of piecewise linear systems equipped with neural network controllers are addressed. The neur…
Reachable Set Computation and Safety Verification for Neural Networks with ReLU Activations
Weiming Xiang, Hoang-Dung Tran, Taylor T. Johnson
Neural networks have been widely used to solve complex real-world problems. Due to the complicate, nonlinear, non-convex nature of neural networks, formal safety guarantees for the…
Output Reachable Set Estimation and Verification for Multi-Layer Neural Networks
Weiming Xiang, Hoang-Dung Tran, Taylor T. Johnson
In this paper, the output reachable estimation and safety verification problems for multi-layer perceptron neural networks are addressed. First, a conception called maximum sensiti…
Order-Reduction Abstractions for Safety Verification of High-Dimensional Linear Systems
Hoang-Dung Tran, Luan Viet Nguyen, Weiming Xiang +1
Order-reduction is a standard automated approximation technique for computer-aided design, analysis, and simulation of many classes of systems, from circuits to buildings. For a gi…